proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
*	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
\|
*	Removed extra parenthesis.	David Aspinall	1999-07-03
\|
*	fixed some regexp via proof-anchor-regexp;	Makarius Wenzel	1999-07-02
\|
*	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
\|
*	Changed read-no-blanks-input to read-string, former is defunct.	David Aspinall	1999-01-12
\|
*	File sent by David von Oheimb.	David Aspinall	1998-12-18
\|
*	Docstring tweak	David Aspinall	1998-12-15
\|
*	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).
*	Fix for splash hack for theory files when proo-splash-inhibit=t.	David Aspinall	1998-12-10
\|
*	Added clear-goals-buffer stuff, asked for response to be left after use_thy.	David Aspinall	1998-11-26
\|
*	Cleaned up, and made use_thy remove ML file from DB properly;	David Aspinall	1998-11-25
\| \| \| \|	optimised use_thy to report only on files newly added to db.
*	Documentation improvements.	David Aspinall	1998-11-25
\|
*	FSF Emacs fix for buffer-file-truename, which is the	David Aspinall	1998-11-25
\| \| \| \|	abbreviated form of file-truename!
*	Fixed show_context	David Aspinall	1998-11-25
\|
*	Fixes to debug long standing not-showing-first-goal problem.	David Aspinall	1998-11-25
\|
*	Added Isamode-like keybinding C-c C-l for proof-prf.	David Aspinall	1998-11-25
\|
*	Docstring fixes, minor improvements.	David Aspinall	1998-11-25
\|
*	Docstring fixes	David Aspinall	1998-11-25
\|
*	Improvements for multiple files and robustness: keep a copy of	David Aspinall	1998-11-20
\| \| \| \|	the initial theory database state, and add a restart command.
*	Improvements for multiple files. Now saves state specially for ProofGeneral.	David Aspinall	1998-11-18
\|
*	Added isa-update function. Altered settings.	David Aspinall	1998-11-18
\|
*	Fixed problem with list_loaded_files and update().	David Aspinall	1998-11-18
\| \| \| \| \| \| \| \| \|	Now when doing use_thy, we don't do an update. Hopefully "following children are out of date" message will be superfluous because they will be unlocked already. Will be re-read as needed. Added update function. Fixed up implementation of list_parents.
*	Added Proof General menu to theory file mode.	David Aspinall	1998-11-18
\|
*	Added clear_response_buffer regexp, use_thy_and_update now in ProofGeneral	David Aspinall	1998-11-18
\|
*	Improvements and cleanups:	David Aspinall	1998-11-18
\| \| \| \| \| \| \| \|	. Put functions into ProofGeneral structure . Annotations around ordinary output appear before cr's . Added clear_response_buffer functionw . Added special_theories to avoid looking up filenames of theories which don't have them
*	new file to factor out improved theory reader junk.	David Aspinall	1998-11-18
\|
*	Bug in regexp	David Aspinall	1998-11-12
\|
*	In a fit of autocracy, removed proof-tags-support, binding for	David Aspinall	1998-11-12
\| \| \| \| \| \|	M-tab and appearance of Find Tags in PG menu. The menu entry already appears in Tools->Tags, and users should bind M-tab for themselves.
*	Fixed error regexp	David Aspinall	1998-11-12
\|
*	Fixed a regexp.	David Aspinall	1998-11-12
\|
*	Replaced custom-set-variables with customize-set-variable:	David Aspinall	1998-11-12
\| \| \| \| \|	the first one sets the saved value for variables, rather than default values.