proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
*	Fix most doc issues raised by (checkdoc)	Erik Martin-Dorel	2018-08-23
\|
*	Update copyright messages and improve the header of elisp files.	Erik Martin-Dorel	2018-02-21
\|
*	Fixing #154.	Pierre Courtieu	2017-02-23
\|
*	fix generic interrupt procedure to interrupt parallel background compilation	Hendrik Tews	2016-12-14
\|
*	proof-retract-command-hook added + more auto adjust width in coq mode.	Pierre Courtieu	2015-10-13
\|
*	proof-assert-command-hook added + Auto adjust width in coq mode.	Pierre Courtieu	2015-10-12
\| \| \| \| \| \| \|	This hook was missing, it allows to send complete commands before the (set of) command(s) sent by the user. It shall be used when proof-shell-insert-hook cannot be used (because of multiple prompts appearing).
*	Fixing 4096 character limit of scomint-send-input.	Pierre Courtieu	2015-10-09
\| \| \| \| \|	Extended the fix of #453 (trac tracker) for emacs 25 (>=24 instead of = 24).
*	cleaned previous commits (generic variable to disable error coloring).	Pierre Courtieu	2015-02-04
\|
*	Fixed response display spurious newlines for coq.	Pierre Courtieu	2014-12-18
\| \| \| \| \| \|	Added an option about that in proof-config. To check: I adapted proof-treee regrexp accordingly.
*	- first version of parallel asynchronous compilation for coq in	Hendrik Tews	2012-11-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	coq-par-compile.el (must be activated via coq-compile-parallel-in-background) - items in the queue region are not necessarily in proof-action-list any more! Require commands and the following items are stored elsewhere until the compilation finishes. Variable proof-second-action-list-active notifies the generic machinery if queue items are stored elsewhere. In this case, Proof General must neither release the proof shell lock nor delete the queue span when proof-action-list is empty. - to kill background processes as early as possible, the new hook proof-shell-signal-interrupt-hook is used
*	proof-shell-process-connection-type: try using pipes by default in Emacs 24,	David Aspinall	2012-09-14
\| \| \| \|	to avoid Trac #453: http://proofgeneral.inf.ed.ac.uk/trac/ticket/453
*	Improve configuration for HOL Light. Allow goals display to be prefixed by ↵	David Aspinall	2012-01-09
\| \| \| \|	ignored junk (val it : goalstack =).
*	proof-shell-end-goals-regexp doc: fix inaccuracy, goals always start	David Aspinall	2012-01-09
\| \| \| \|	at start of proof-shell-start-goals-regexp.
*	merge ProofTreeBranch into main trunk:	Hendrik Tews	2012-01-03
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- 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
*	fix a log of broken customization types	Hendrik Tews	2011-12-06
\|
*	Quick stab at support for switching to proof shell when interactive support ↵	David Aspinall	2011-11-15
\| \| \| \|	expected, see Trac #430
*	To fix pgshell mode, restore proof-shell-insert support for a single string ↵	David Aspinall	2011-10-13
\| \| \| \|	argument and allow nil setting for proof-shell-start-goals-regexp.
*	- flushed proof-done-advancing-require-function and	Hendrik Tews	2011-05-05
\| \| \| \| \|	proof-shell-require-command-regexp - TAGS updated to really flush them
*	proof-shell-insert-hook: Clean docstring, addressing #396.	David Aspinall	2011-04-13
\|
*	Make proof-shell-quit-timeout a prover-specific customize option, default to ↵	David Aspinall	2011-01-23
\| \| \| \|	45 for Isar. See http://proofgeneral.inf.ed.ac.uk/trac/ticket/384.
*	Fix typo	David Aspinall	2011-01-23
\|
*	- fixed compilation errors	Hendrik Tews	2011-01-18
\|
*	- move proof-no-fully-processed-buffer to generic/proof-config	Hendrik Tews	2011-01-14
\| \| \| \| \| \|	- add documentation for it - add a test case demonstrating it in coq/ex/test-cases/retract-completely-asserted
*	Add preliminary support for multiple files for coq.	Hendrik Tews	2011-01-12
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The following points are implemented already: - recompile either via an external command (make) or let ProofGeneral handle everything internally - complete dependency tracking and recompilation for coq files in internal mode - support for extending the LoadPath: does almost work, even if specified file-locally - move back to clean state if recompilation fails There are the following known problems: - coq-load-path extensions are not retracted - fails on partially qualified library names
*	Patch to add pgipfloat type.	David Aspinall	2010-12-16
\|
*	Support proof-shell-init-cmd being a list	David Aspinall	2010-09-29
\|
*	Replace proof-terminal-char with proof-terminal-string.	David Aspinall	2010-08-27
\|
*	Reduce quit timeout to sensible value	David Aspinall	2010-08-24
\|
*	proof-shell-process-connection-type: Revert to long-lived previous default ↵	David Aspinall	2010-08-19
\| \| \| \|	of t (for safety, no ill behaviour observed)
*	proof-shell-process-connection-type: remove near obsolete test and text	David Aspinall	2010-08-18
\| \| \| \| \| \|	about Solaris. Experiment using pipe instead of pty communication as default now scomint buffer not intended for interactive input and runs prover process directly.
*	Clean up handling of pending interrupts, remove experimental ↵	David Aspinall	2010-08-17
\| \| \| \|	proof-shell-interrupts-after-commit.
*	proof-shell-interrupts-after-commit: support commit-before-interrupt mode ↵	David Aspinall	2010-08-15
\| \| \| \|	[experimental/temporary].
*	Checkdoc cleanups	David Aspinall	2010-08-08
\|
*	docstring	David Aspinall	2009-12-04
\|
*	Replace proof-locked-end -> proof-unprocessed-begin	David Aspinall	2009-11-30
\|
*	even higher proof-shell-quit-timeout -- saving main HOL takes 20s on a ↵	Makarius Wenzel	2009-11-30
\| \| \| \|	fast machine;
*	raised proof-shell-quit-timeout to accomodate bulky write-back images;	Makarius Wenzel	2009-11-29
\|
*	Remove doc mention of obsolete function `pg-assoc-analyse-structure'.	David Aspinall	2009-11-28
\|
*	proof-script-use-old-parser: remove configuration option and cleanup	David Aspinall	2009-10-15
\|
*	Remove `next-entity' settings for func-menu.	David Aspinall	2009-10-14
\|
*	Typo	David Aspinall	2009-09-28
\|
*	Functions find-and-forget and count-undos now return lists of commands	David Aspinall	2009-09-28
\|
*	Fix docs	David Aspinall	2009-09-11
\|
*	Experimental changes to queue several commands at once and to allow ↵	David Aspinall	2009-09-10
\| \| \| \|	pre-processing of commands when they're queued from script
*	Clean compile	David Aspinall	2009-09-10
\|
*	Add proof-shell-font-lock-keywords, proof-arbitrary-undo-positions	David Aspinall	2009-09-09
\|
*	p-s-classify-output -> p-s-handle-output, and simplify system-specific hook	David Aspinall	2009-09-09
\|
*	proof-shell-quiet-errors: move to user opts custom group	David Aspinall	2009-09-09
\|
*	proof-kill-goal-command: default to nil, not empty string	David Aspinall	2009-09-08
\|
*	Remove barely useful proof-shell-abort-goal-regexp (only served to sanitize ↵	David Aspinall	2009-09-08
\| \| \| \|	LEGO messages)