proof-general - Emacs plugins for proof management systems

Age	Commit message (Collapse)	Author
2020-06-04	New hook for early prompt/output analyzis.	Pierre Courtieu
	proof-state-change-pre-hook happens earlier than proof-state-change-hook, i.e. before proof-done-advancing. This should be used to register information in the currently processed span before proof-done-advancing classifies it. Historically PG design was to gather these information during proof-done-advancing (or in its hook called at the end) by just looking at the command statement. But it is often useful to look at the output (messages and/or prompt) to gather more accurate information. Some of this information may be needed DURING proof-done-advancing. Hence this early hook.
2018-12-13	Use `cl-lib` instead of `cl` everywhere	Stefan Monnier
	Use lexical-binding in a few files where it was easy. Don't require `proof-compat` when it's not used. * coq/coq-db.el: Use lexical-binding. * coq/coq-system.el: Use lexical-binding. (coq--extract-prog-args): Use concatenated-args rather than recomputing it. * coq/coq.el: Require `span` to silence some warnings. * generic/pg-user.el: Use lexical-binding. (complete, add-completion, completion-min-length): Silence warnings. * generic/pg-xml.el: Use lexical-binding. (pg-xml-string-of): Prefer mapconcat to reduce+concat. * generic/proof-depends.el: Use lexical-binding. (proof-dep-split-deps): Use `push`. * generic/proof-shell.el: Require `span` to silence some warnings. (proof-shell-invisible-command): Don't use lexical-let just to build a wasteful η-redex! * lib/holes.el: Use lexical-binding. Remove redundant :group args. * lib/span.el: Use lexical-binding. (span-read-only-hook): Use user-error. (span-raise): Remove, unused.
2018-08-23	Fix most doc issues raised by (checkdoc)	Erik Martin-Dorel

2018-02-21	Update copyright messages and improve the header of elisp files.	Erik Martin-Dorel

2017-05-05	Change (eval-when (compile) ...) to (eval-when-compile ...)	Clément Pit--Claudel
	This fixes a bunch of compilation warnings
2017-01-14	Fix prooftree for Coq 8.6	Hendrik Tews
	In Coq 8.6 evar status printing is off by default, causing prooftree to crash. This patch inserts invisible commands to switch evar status printing on and off. This is done via the urgent-action-hook.
2016-12-28	fix prooftree crash with long evar lines	Hendrik Tews

2013-01-21	- implement proof-script insertion	Hendrik Tews

2013-01-20	- implement retract from prooftree	Hendrik Tews

2013-01-17	- support Grab Existential Variables for Prooftree	Hendrik Tews
	- protocol change, but stay at version 3
2013-01-15	- support bullets and braces in Prooftree	Hendrik Tews
	- prooftree protocol change to version 3
2012-09-12	treat #450 by requiring that proofs are started with Proof	Hendrik Tews

2012-01-19	Typo	David Aspinall

2012-01-04	* fix case where some existential is instantiated with the last proof command	Hendrik Tews
	* protocol change - rename proof-complete into proof-finished and add existential info - add proof-complete message
2012-01-03	merge ProofTreeBranch into main trunk:	Hendrik Tews
	- 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