proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
*	Add universal keys to theory mode	David Aspinall	1999-11-29
\|
*	Fix to proof-shell-proof-completed-regexp by reverting to previous version.	David Aspinall	1999-11-26
\|
*	Patch to proof-shell-proof-completed-regexp to prevent overflow, sent by Markus	David Aspinall	1999-11-23
\|
*	Failed attempt to trap C-g during try-update-thy. Left as comments.	David Aspinall	1999-11-18
\|
*	Remove some obsolete/unecessary stuff.	David Aspinall	1999-11-17
\|
*	Cleanups and a bit more highlighting	David Aspinall	1999-11-16
\|
*	Matching goals regexp. Comments.	David Aspinall	1999-11-16
\|
*	Removed font-lock settings. Set proof-font-lock-zap-commas=t	David Aspinall	1999-11-15
\|
*	Many robustness improvements for error and interrupt handling:	David Aspinall	1999-11-14
\| \| \| \| \| \| \| \| \| \| \| \|	- Introduce proof-shell-error-or-interrupt-seen flag set after an error or interrupt was seen (in fact, on every call to proof-release-lock). Examine it in proof-activate-scripting to see whether hooks succeeded in activating scripting. - Test in the shell filter for the lock being held yet nothing in the action list, and clear the lock if so. Gets rid of repetetive proof-shell-busy messages when the queue is empty (for errors during development, or nasty uses of C-g) - Add a timeout to proof-shell-wait (not used yet)
*	proof-nested-goals-allowed -> proof-completed-proof-behaviour	David Aspinall	1999-11-14
\| \| \| \| \|	Patch for more flexible handling of closing goal...save regions after proof has been completed.
*	Fixes for Isabelle in case theory file is visited before script file.	David Aspinall	1999-11-12
\|
*	Display qed message in goals buffer	David Aspinall	1999-11-12
\|
*	Extensive fixes for x-symbol and font-lock.	David Aspinall	1999-11-11
\|
*	Fixes for x-symbol activation/deactivation strings	David Aspinall	1999-11-09
\|
*	Arrange for activate-scripting to not block for interactive calls.	David Aspinall	1999-11-09
\|
*	Comments.	David Aspinall	1999-11-08
\|
*	Typo.	David Aspinall	1999-11-08
\|
*	Changed web page to official one.	David Aspinall	1999-11-08
\| \| \| \|	Added x-symbol support (moved here from generic/proof-x-symbol)
*	improved proof-shell-error-regexp;	Makarius Wenzel	1999-10-29
\|
*	isa-update-thy-only: 'try' option;	Makarius Wenzel	1999-10-27
\|
*	ProofGeneral.inform_file_processed/retracted;	Makarius Wenzel	1999-10-26
\| \| \| \|	improved proof-shell-compute-new-files-list (more robust);
*	tuned proof-shell-error-regexp;	Makarius Wenzel	1999-10-26
\|
*	Changed name of proof-shell-cd-cmd for uniformity.	David Aspinall	1999-10-21
\|
*	Add isa-shell-update-thy at the end of proof-activate-scripting-hook.	David Aspinall	1999-10-20
\|
*	Added uncaught exception to error-regexp	David Aspinall	1999-10-19
\|
*	Rename proof-mark-buffer-atomic->proof-complete-buffer-atomic.	David Aspinall	1999-10-19
\|
*	Deactivate scripting before retracting a theory file. Fix for DvO's report.	David Aspinall	1999-10-19
\|
*	Whitespace	David Aspinall	1999-10-15
\|
*	Fix for state-preserving-p	David Aspinall	1999-10-06
\|
*	Made new command proof-cd to cd to the directory of the current	David Aspinall	1999-10-06
\| \| \| \| \| \|	buffer. Added a version of it to proof-activate-scripting-hook. Removed cd from initialization sequence. Changed prover specifics accordingly.
*	Turned off C-c C-l; fixed syntax for old result form; proof-showproof-command.	David Aspinall	1999-10-06
\|
*	thy mode binding made to match with script mode	David Aspinall	1999-10-06
\|
*	Renamed some configuration variables for uniformity, see CHANGES.	David Aspinall	1999-10-01
\|
*	replaced isa-output-font-lock-terms by isa-output-font-lock-keywords-1;	Makarius Wenzel	1999-09-30
\|
*	Enabled hack for proof-shell-leave-annotations-in-output	David Aspinall	1999-09-29
\|
*	Added setting for proof-find-theorems-command.	David Aspinall	1999-09-23
\|
*	improved (?) proof-shell-proof-completed-regexp;	Makarius Wenzel	1999-09-22
\|
*	Adjusted proof-shell-proof-completed-regexp to match against whole of	David Aspinall	1999-09-21
\| \| \| \| \|	proofstate output including "No subgoals!" message. Now PG can correctly set the proof-shell-proof-completed flag.
*	Maintainer addresses	David Aspinall	1999-08-23
\|
*	fixed comment;	Makarius Wenzel	1999-08-23
\|
*	Added font-lock keywords and syntax table setup for buffers displaying	David Aspinall	1999-08-23
\| \| \| \|	Isabelle output.
*	eliminated superficial ';'s;	Makarius Wenzel	1999-08-20
\|
*	proof-shell-start-goals-regexp: include \n;	Makarius Wenzel	1999-08-18
\| \| \| \| \|	isa-init-syntax-table moved to isa-syntax.el; improved isa-update-thy-only;
*	proof-shell-first-special-char ?\350;	Makarius Wenzel	1999-08-16
\| \| \| \| \| \| \| \|	tuned prompt; deactivated "No subgoals!"; use Isabelle's native ProofGeneral.init; proper setup for theory loader actions: better handling of multiple buffers; isa-find-and-forget does nothing;
*	renamed proof-commands-regexp to proof-indent-commands-regexp, which	Makarius Wenzel	1999-05-27
\| \| \| \|	is less confusing);
*	fixed syntax entry for "_"	Thomas Kleymann	1999-02-03
\|
*	Regexp bug. Use proof-string-match appropriately.	David Aspinall	1999-02-01
\|
*	Fixed broken check on proof-mode-hook.	David Aspinall	1998-12-15
\|
*	made many minor changes to the documentation	Thomas Kleymann	1998-12-15
\|
*	Altered behaviour to allow retraction part-way through finished scripts.	David Aspinall	1998-12-11
\| \| \| \| \| \| \| \|	Previously Proof General was asked to unlock a file A.ML as soon as retraction in it happened. Now Proof General is only asked to unlock the children of A.ML, although Isabelle records the fact that A.ML has been retracted. (Which means that if A.ML is later re-linked, Proof General will correctly get told about it).