| Age | Commit message (Collapse) | Author |
|---|
|
|
|
unparseable
|
|
|
|
|
|
|
|
|
|
|
|
|
|
command elements.
|
|
|
|
|
|
|
|
|
|
|
|
proof-inside-string: added
|
|
|
|
(see http://proofgeneral.inf.ed.ac.uk/trac/ticket/293)
|
|
|
|
needed here (possible Emacs bug)
|
|
|
|
pg-last-output-displayform: protect against single \n in last output
|
|
(if proof-follow-mode suggests following locked region)
|
|
on any edit (affects error spans and outdated help spans).
|
|
comment, not a command.
|
|
|
|
proof-assert-electric-terminator: restore expected behaviour with/without term.
|
|
|
|
|
|
improvements
|
|
|
|
pre-processing of commands when they're queued from script
|
|
(mask current bug in Coq code)
|
|
|
|
to tidy up popups for Isabelle.
|
|
|
|
proof-script-delete-spans: leave 'pghelp spans in place for now
pg-set-span-helphighlights: add extra FACE argument
proof-done-advancing-save, proof-make-goalsave: support proof-arbitrary-undo-positions.
|
|
as per previous proof-shell update.
|
|
|
|
proof-activate-scripting: minor cleanup
proof-assert-until-point: don't go back beyond end of locked
|
|
alter meaning of `proof-only-whitespace-to-locked-region-p';
both now refer to char after point.
Script elements are now stored in hash tables rather than lists.
|
|
|
|
replaces)
proof-done-advancing: remove spurious first case
proof-assert-until-point: don't move point, restore intuitive
behaviour when on whitespace between unprocessed commands
(process preceding commands only)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
