proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
*	fixed proof-shell-error-regexp;	Makarius Wenzel	2000-02-07
\|
*	Comments	David Aspinall	2000-01-12
\|
*	Fixes for short output duplication problem: set ↵	David Aspinall	2000-01-06
\| \| \| \|	proof-shell-eager-annotation-start-length.
*	Change SML minor mode binding to C-c C-m, avoiding clash with	David Aspinall	1999-11-29
\| \| \| \| \|	proof-interrupt-process. Add commands from proof-universal-keys to menu, and add all of proof-shared-menu.
*	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
\|
*	Made thy-indent-level a user opt.	David Aspinall	1999-11-24
\|
*	Patch to proof-shell-proof-completed-regexp to prevent overflow, sent by Markus	David Aspinall	1999-11-23
\|
*	tuned faces;	Makarius Wenzel	1999-11-22
\|
*	Added by defvars x-symbol-isa-name, x-symbol-isa-modeline-name so can use ↵	David Aspinall	1999-11-19
\| \| \| \|	this file without PG
*	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)
*	More highlighting	David Aspinall	1999-11-14
\|
*	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.
*	More theory file sections	David Aspinall	1999-11-12
\|
*	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
\|
*	Next round of fixups for font-lock and x-symbol.	David Aspinall	1999-11-11
\|
*	Extensive fixes for x-symbol and font-lock.	David Aspinall	1999-11-11
\|
*	Removed unsociable key-bindings.	David Aspinall	1999-11-10
\|
*	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
\|
*	isa-keywords-save: removed "result";	Makarius Wenzel	1999-10-26
\| \| \| \| \| \|	isa-keywords-commands: added "ProofGeneral.repeat_undo"; added isa-keywords-proof-commands; added isa-verbatim;
*	update by DvO;	Makarius Wenzel	1999-10-22
\|
*	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
\|
*	let PROOFGENERAL_ASSISTANTS control isa vs. isar selection;	Makarius Wenzel	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
\|
*	tuned isa-init-output-syntax-table;	Makarius Wenzel	1999-09-30
\| \| \| \| \| \|	removed isa-binder-regexp (obsolete); remove isa-font-lock-terms; proper isa-output-font-lock-keywords-1;
*	Enabled hack for proof-shell-leave-annotations-in-output	David Aspinall	1999-09-29
\|