| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
span regions.
|
|
|
|
|
|
|
|
|
|
(i.e., automatic preview of next command)
|
|
|
|
interrupting if prover is busy before undoing. Refs Trac #293
|
|
|
|
support this.
|
|
|
|
proof-shell-interrupts-after-commit.
|
|
|
|
|
|
proof-activate-scripting-hook does nothing (case: switching buffers in
Coq when there was an error)
|
|
|
|
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)
|
|
|
