| Age | Commit message (Collapse) | Author |
|---|
|
|
|
pg-last-output-displayform: protect against single \n in last output
|
|
|
|
and self-delete.
|
|
|
|
(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
|
|
proof-script
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
commands (certainly when the value is persisted).
|
|
|
|
pre-processing of commands when they're queued from script
|
|
(mask current bug in Coq code)
|
|
|
|
|
|
|
|
fix requires.
|
|
|
|
|
|
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.
|
