| Age | Commit message (Collapse) | Author |
|---|
|
|
|
to be made into a local variable.
|
|
|
|
|
|
|
|
- added a link to the library and the reference card for version 1.3
|
|
|
|
o monitoring the end of imports is now implemented via
a new proof-shell-process-output-system-specific hook
|
|
proof-config-done.
|
|
proof-locked-span if they don't already exist.
Call generic span function for making spans read-only.
|
|
unprocessed region. This should be used instead of proof-locked-end
if we're not guaranteed to be in scripting buffer.
proof-locked-end now calls proof-unprocessed-begin if we're in the
proof-script-buffer.
We set the goal name to "Unnamed_thm" if we can't find any other name
for the theorem.
proof-process-active-terminator now calls proof-unprocessed-begin.
proof-shell-config-done now calls 'proof-mode-hook.
|
|
Emacs (19.34)
o adjusting the directory (at least for LEGO) must not contain "~". We
now expand `default-directory' before cding to it. [Under XEmacs
(unlike Emacs 19.34), `default-directory' is already in expanded form.]
|
|
Pascal Brisset's suggestion.
|
|
|
|
proof-goto-end-of-locked, and proof-goto-end-of-locked now doesn't
switch buffer.
Added code in proof-steal-process to handle case of stealing script
management from a killed buffer.
Set proof-active-buffer-fake-minor-mode to nil in
proof-restart-script.
|
|
proof-count-undos and proof-find-and-forget.
Generalized proof-shell-analyse-structure, introduced variable
proof-analyse-using-stack.
Generalized proof menu plus ancillary functions.
Generalized proof-mode-version-string.
Removed emacs-version-at-least.
Removed comment about buffer-display-table.
Moved various comments into documentation string.
Fixed another mode-line command for emacs19.
|
|
|
|
o support indentation of commands
o replaced test of Emacs version with availability test of specific
features
o C-c C-c, C-c C-v and M-tab is now available in all buffers
|
|
proof-done-trying deletes the spans that were created
|
|
o employed `Info-default-directory-list' rather than
`Info-directory-list' so that code also works for Emacs 19.34
o setting of `Info-default-directory-list' now at proof level
|
|
|
|
Changed some if's without then-clauses to and's.
Removed (proof-detach-segments) from (proof-steal-process)
This is the bug that made changing buffers fail in emacs19:
the segments had already been detached.
Check if we're in proof buffer for proof-frob-locked-end.
Force mode-line update for emacs19 in proof-active-terminator-minor-mode.
|
|
nothing is changed.
Changed proof-indent-region code so that the endpoints of the region
being indented change as indentation is done: it was infinite looping
because the end could never be reached.
|
|
and span-overlay.el. Definitions of proof-queue-span and
proof-locked-span now in proof.el.
Changed variable names [s]ext to span.
|
|
|
|
Made proof-assistant specific code into separate procedure,
proof-parse-indent.
Separated consideration of {}'s so it only happens for LEGO.
|
|
Fixed problem with active terminator mode: [proof-terminal-char] isn't
the same as (vector proof-terminal-char).
|
|
|
|
introduces error messages.
Put cd before init in proof-shell-config-done (this won't work for
Coq).
|
|
Also includes some changes for "Definition" problem in Coq, where
Definition couldn't be used for proof scripts.
Finally, modified proof-dependencies-xemacs code to fix problem that
undoing to (point-min) meant you couldn't type at first character.
|
|
|
|
|
|
to the way errors are handled, so that any delayed output is inserted
in the buffer before the error message is printed.
|
|
proof-assistant-dependent variables.
Added ctrl-button1 to copy selected region to end of locked region
|
|
o bound C-c C-z to 'proof-frob-locked-end
|
|
|
|
proof-goto-end-of-locked-if-pos-not-visible-in-window (also new)
o proof-find-next-terminator now also works inside a locked region
o implemented proof-process-buffer which is by default bount to C-c C-b
|
|
o If proof-retract-until-point is is invoked outside a locked region,
the last successfully processed command is undone.
o Added support for func-menu
|
|
|
|
active lemmas.
Separated proof-lift-global as separate command to lift global
declarations above active lemmas.
Fixed usual problem that 'cmd is nil for comments in this code.
Made lifting globals start from beginning of file rather than go
backwards.
Fixed bug in pbp code proof-shell-analyse-structure, where stack
wasn't cleared for new goal-hyp's.
|
|
proof-interrupt-process. Added moving nested lemmas above goal for coq.
Changed the key mapping for assert-until-point to C-c RET.
|
|
|
|
|
|
of ^G's from comint-get-old-input for some inexplicable reason.
|
|
Coq goals which start with text rather than simply ?n
Updated 'let (ap 0)' in proof-shell-analyse structure, to be slightly
more compatible with Coq pbp code
|
|
o fixed a bug in proof-done-retracting
|
|
* pbp-goal-command and pbp-hyp-command use proof-terminal-string
* updates to keywords
* fix for goal regexp
|
|
|
|
Hence, << Cd "../x". >> works in Coq, and
<< echo "hello; world"; >> should work in LEGO
But maybe we don't want "Cd"'s at all...
|
|
continuous pbp-buffer update bug.
|
