| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Fixed bug in add-span and remove-span concerning return value of
span-traverse.
|
|
|
|
proof-locked-span if they don't already exist.
Call generic span function for making spans read-only.
|
|
proof-lock-span is often changed and has starting point 1.
Factored out common code of add-span and remove-span into
span-traverse.
|
|
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.
|
|
|
|
particular to LEGO, and call it from lego-shell-mode-config.
|
|
particular to coq.
Changed proof-ctxt-string to "Print All".
Call coq-init-syntax-table from coq-shell-mode-config. This was
necessary to get prompts with "'"s in them (coming from goals with
same) recognized.
|
|
Changed "\\s " into "\\s-" as whitespace pattern.
|
|
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.
|
|
Added Fix, Destruct and Cofix as tactics.
Added Local as goal.
|
|
Added definitions of foldr and foldl if they aren't already loaded.
Changed definitions of add-span, remove-span and find-span-aux to be
non-recursive.
Removed detach-extent since this file isn't used by xemacs.
Added function append-unique to avoid repetitions in list generated by
spans-at-region.
Changed next-span so it uses member-if.
|
|
|
|
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.
|
|
Changed some variables to their associated constant in cases where we
know they must be equal.
|
|
|
|
Added item that we need to write proof-retract-file.
|
|
|
|
|
|
|
|
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.
|
|
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.
Moved various comments into documentation string.
|
|
|
|
|
|
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.
|
|
|
|
|
|
Added problem of buffers and need for incremental adding of tactics in
Coq.
|
|
Removed span-at-type.
Fixed bug in span-at-before, where (span-start span) may be nil.
Added spans-at-(point|region)[-prop], which fixes bug of C-c u at end
of buffer.
|
|
Added comments about current state of emacs19 port.
|
|
Fixed set-span-endpoints so it preserves invariant.
Changed add-span and remove-span so that they update last-span
correctly themselves, and don't take last-span as an argument.
|
|
|
|
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.
|
|
|
|
part of a hook. This change has been caused by replacing
`proof-shell-config' with `proof-shell-insert-hook'
|
|
|
|
and span-overlay.el.
This file was developed under xemacs, but runs for emacs19 as well.
|
|
and span-overlay.el.
This file was developed for xemacs.
|
|
and span-overlay.el. Definitions of proof-queue-span and
proof-locked-span now in proof.el.
Changed variable names [s]ext to span.
|
|
and span-overlay.el.
|
|
|
