proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
*	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).
*	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
\|
*	FSF Emacs fix for buffer-file-truename, which is the	David Aspinall	1998-11-25
\| \| \| \|	abbreviated form of file-truename!
*	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
\|
*	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.
*	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 clear_response_buffer regexp, use_thy_and_update now in ProofGeneral	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
\|
*	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.
*	Disabled problematic requires temporarily.	David Aspinall	1998-11-10
\|
*	Removed references of proof-shell-noise-regexp	Thomas Kleymann	1998-11-10
\|
*	Fixes for byte compilations and missing bits of Isamode.	David Aspinall	1998-11-10
\|
*	Removed superfluous variable. Improved docstrings.	David Aspinall	1998-11-09
\|
*	Added key binding to switch between theory and ML files.	David Aspinall	1998-11-04
\|
*	Disabled annotated prompts because of strange bug.	David Aspinall	1998-11-03
\|
*	Work on improving regular expressions for Isabelle.	David Aspinall	1998-11-03
\|
*	fixed minor bugs	Thomas Kleymann	1998-11-02
\|
*	Fixes for multiple files. More defcustoms.	David Aspinall	1998-10-29
\|
*	Crudely hacked Isabelle image onto splash screen.	David Aspinall	1998-10-29
\|
*	Begun work on adding more special annotations for Isabelle.	David Aspinall	1998-10-29
\|
*	More hacks to variable names for customize (sorry)	David Aspinall	1998-10-29
\|
*	Improved behaviour of Isabelle multiple files: don't retract parent theory.	David Aspinall	1998-10-28
\|
*	Fixed bug in Isabelle count undos. Now uses undo instead of choplev.	David Aspinall	1998-10-28
\|
*	Mods for cleaner byte compile	David Aspinall	1998-10-27
\|
*	Begun work on clean byte compilation / clarifying interfaces.	David Aspinall	1998-10-27
\|
*	Fixed urgent message stuff. proof-shell-process-urgent-messages	David Aspinall	1998-10-27
\| \| \| \|	now seems to correctly observe all messages which pass through.
*	Renamed proof-invisible-command proof-shell-invisible-command.	David Aspinall	1998-10-27
\| \| \| \| \| \| \|	Removed superfluous optional 'relaxed' argument from: proof-shell-invisibile-command, proof-grab-lock, proof-start-queue.
*	Work on Isabelle theory reader.	David Aspinall	1998-10-27
\|