proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
*	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
\|
*	Added setting for proof-find-theorems-command.	David Aspinall	1999-09-23
\|
*	tuned example according to Isabelle style-guide;	Makarius Wenzel	1999-09-22
\|
*	improved (?) proof-shell-proof-completed-regexp;	Makarius Wenzel	1999-09-22
\|
*	Fix for proof-shell-proof-completed-regexp	David Aspinall	1999-09-21
\|
*	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.
*	Cleaned up example files so all demonstrate same theorem "conj_comms".	David Aspinall	1999-09-13
\| \| \| \| \|	Would be nice to add more theorems to compare scripts in different systems.
*	added bind_thms;	Makarius Wenzel	1999-09-03
\| \| \| \| \| \| \|	added no_qed; more tacticals; removed isa-tactics (didn't make much sense); isa-goal-command-regexp accomodates "val ... =" part;
*	usage: tell PROOFGENERAL_OPTIONS;	Makarius Wenzel	1999-09-03
\| \| \| \|	-u true by default;
*	added ALLGOALS;	Makarius Wenzel	1999-08-29
\|
*	added qed_spec_mp;	Makarius Wenzel	1999-08-25
\|
*	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.
*	Improved syntax by copying from isar-syntax.el.	David Aspinall	1999-08-23
\| \| \| \|	Begun on section for Isabelle output syntax.
*	Disabled binder regexp font locking	David Aspinall	1999-08-20
\|
*	eliminated superficial ';'s;	Makarius Wenzel	1999-08-20
\|
*	update by DvO;	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;
*	isa-init-syntax-table moved here from isa.el;	Makarius Wenzel	1999-08-18
\|
*	replaced 'ProofGeneral' by 'Proof General';	Makarius Wenzel	1999-08-18
\|
*	obsolete;	Makarius Wenzel	1999-08-18
\|
*	obsolete, use Isabelle's native ProofGeneral.init instead;	Makarius Wenzel	1999-08-16
\|
*	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;
*	tuned;	Makarius Wenzel	1999-08-06
\|
*	ProofGeneral interface wrapper for Isabelle/classic	Makarius Wenzel	1999-08-06
\|