| Age | Commit message (Collapse) | Author |
|
|
|
- add support for proof-tree displays (currently Coq only)
- new file generic/proof-tree.el contains generic code
- Coq specific code has been added to coq/coq.el
Changes to existing Proof General functions:
- proof-shell-exec-loop and proof-shell-filter-manage-output call
proof-tree display functions, when the proof-tree display is on
- proof-shell-exec-loop returns t if proof-action-list is empty
_or_ contains only items for updating the proof-tree
- proof-shell-should-be-silent returns nil when the proof-tree
display is on
- coq-last-prompt-info, coq-last-prompt-info-safe return as
additional 4th element the name of the current proof
|
|
interactive-p with called-interactively-p)
|
|
|
|
Emacsen, displayed in Emacs 24 UI)
|
|
who read or edit by waving mouse at text
|
|
defaults
|
|
and keep possibly customized variables bound. Closes Trac #387.
|
|
|
|
|
|
|
|
|
|
Martin-Dorel)
|
|
convenience commands.
|
|
(i.e., automatic preview of next command)
|
|
|
|
with holes
mode (unfortunately).
|
|
|
|
|
|
|
|
|
|
|
|
|
|
command elements.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
pre-processing of commands when they're queued from script
|
|
fix requires.
|
|
Add "Beep on Errors" setting to menu
|
|
|
|
|
|
|
|
|
|
|
|
|