| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
proof-complete-buffer-atomic: simplify.
Add debug message for parser cache.
|
|
|
|
|
|
|
|
|
|
(i.e. files locked by Require). Some progress towards #363,
and at least stops an ugly type error when a Require'd file
is retracted.
|
|
Otherwise we only see first word of symbols using underscores!
|
|
|
|
after it as well as before,
as in PG 3.7. Fixes #371.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
#357). Docstring cleanups.
|
|
|
|
Martin-Dorel)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
auto sending: improve messages, bind autosend-running flag lexically in case of errors
query identifier: use history variable, remove key bindings
|
|
|
|
|
|
span-make-self-removing-span: rename from span-add-self-removing-span
|
|
This means that certain display actions will always be avoided for non-scripting
commands (i.e., hints, anything in `proof-shell-error-or-interrupt-hook').
|
|
in background)
|
|
proof-shell-error-or-interrupt-hook is only invoked for plain script commands.
|
|
input (no non-nil flags in queue)
|
|
|
|
|
|
|
|
prover specific.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
