proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
*	documented LEGO specific bug	Thomas Kleymann	1998-12-16
\|
*	minor changes in the History	Thomas Kleymann	1998-12-16
\|
*	. clarified history of multiple files	Thomas Kleymann	1998-12-16
\| \| \| \|	. added UITP reference
*	Docstring tweak	David Aspinall	1998-12-15
\|
*	Changed title of Chap 10.	David Aspinall	1998-12-15
\|
*	Set version tag for new release.	David Aspinall	1998-12-15
\|
*	Preface: Added David von Oheimb to credits. Mentioned adding multiple files.	David Aspinall	1998-12-15
\|
*	Updated magic.	David Aspinall	1998-12-15
\|
*	Used authorized keywords.	David Aspinall	1998-12-15
\|
*	Docstring fix.	David Aspinall	1998-12-15
\|
*	Made preface unnumbered. Cosmetic improvements. Updated magic.	David Aspinall	1998-12-15
\|
*	Docstring fixes	David Aspinall	1998-12-15
\|
*	Docstring fix	David Aspinall	1998-12-15
\|
*	credits now at the beginning	Thomas Kleymann	1998-12-15
\|
*	Another todo idea added. This version sent to Emacs news groups.	David Aspinall	1998-12-15
\|
*	Idea for magical texi-docstring property for symbols to escape auto markup.	David Aspinall	1998-12-15
\|
*	Documented markup rules and usage at start of package.	David Aspinall	1998-12-15
\|
*	Improved documentation of proof-included-files-list.	David Aspinall	1998-12-15
\|
*	* empty log message *	Thomas Kleymann	1998-12-15
\|
*	Added ps to make all.	David Aspinall	1998-12-15
\|
*	Fixed several typos.	David Aspinall	1998-12-15
\| \| \| \| \| \|	Added docstring for proof-deactivate-scripting and mentioned it in Chap 10. Removed spurious mention of defunct function proof-restart-scripting.
*	Updated magic. Small changes in Chap 11.	David Aspinall	1998-12-15
\|
*	Added back magic target, handy to force update of magic.	David Aspinall	1998-12-15
\|
*	Removed done stuff. Added LEGO cd hook todo.	David Aspinall	1998-12-15
\|
*	radical new version of Credits and References section	Thomas Kleymann	1998-12-15
\|
*	Fixed broken check on proof-mode-hook.	David Aspinall	1998-12-15
\|
*	Removed bogus duplicate call of proof-mode-hook at end of proof-config-done.	David Aspinall	1998-12-15
\|
*	Fixes for FSF Emacs handling of processes, kill buffer hooks,	David Aspinall	1998-12-15
\| \| \| \|	and live/dead overlays.
*	made many minor changes to the documentation	Thomas Kleymann	1998-12-15
\|
*	Altered order of new para and removed some mailing list addrs	David Aspinall	1998-12-14
\|
*	Another FSF bug found in the new filter functions, this time for script buffer.	David Aspinall	1998-12-14
\|
*	Gave up on buggy Emacs 19 support, now give error for Emacs 19.	David Aspinall	1998-12-14
\|
*	Reordered require of cl. Changed deflocal definition.	David Aspinall	1998-12-14
\|
*	Log of testing results.	David Aspinall	1998-12-14
\|
*	. modified mailing lists	Thomas Kleymann	1998-12-14
\| \| \| \|	. added further benefit in last section
*	rearrange pages automatically	Thomas Kleymann	1998-12-14
\|
*	fixed bug in lego-shell-adjust-line-width (It now monitors the	Thomas Kleymann	1998-12-14
\| \| \| \|	proof-goals-buffer)
*	Added section for UITP/TP researchers, mentioning further possible	David Aspinall	1998-12-14
\| \| \| \| \| \| \|	projects. Added many more mailing list addresses. Not sure what half of them are, need vetting really.
*	Set version tag for new release.	David Aspinall	1998-12-11
\|
*	More comments about multiple file problems	David Aspinall	1998-12-11
\|
*	Disabled hack for proof-shell-process-file which allowed	David Aspinall	1998-12-11
\| \| \| \| \| \| \| \| \| \| \|	empty string to stand for filename of current scripting buffer. This added the current script buffer onto the included files list immediately processing it began (if it began with something creating a mark). However, I removed the check for the current scripting buffer so that that could correctly be marked atomic for Isabelle at other times. This resulted in current buffer being marked atomic, and errors. Are there still more errors?
*	Comments	David Aspinall	1998-12-11
\|
*	Urgent fix for multiple files wanted.	David Aspinall	1998-12-11
\|
*	Allow even the current scripting buffer to be marked atomically	David Aspinall	1998-12-11
\| \| \| \| \|	in case the prover asks it to be. This can happen when loading theory files in Isabelle.
*	More test cases mentioned	David Aspinall	1998-12-11
\|
*	todo for Isabelle multiple files.	David Aspinall	1998-12-11
\|
*	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).
*	Added new test/comments.	David Aspinall	1998-12-11
\|
*	Updates	David Aspinall	1998-12-11
\|
*	Several changes:	David Aspinall	1998-12-11
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	1. save-some-buffers now skips the current active scripting buffer. It was annoying to be asked whether to save this one as the user may have just begun typing into a fresh file, or may want to experiment with a modified proof, for example. 2. proof-deactivate-scripting improved so it works pretty well as a (so far undocumented) command. Kill buffer function now removes spans, so that they remain if we deactivate without killing. Plan is to call this in proof-activate-scripting to turn off current scripting buffer and munge the processed file list the way we like it. 3. In both proof-deactivate-scripting and proof-activate-scripting, we do the same thing: files with empty locked regions are removed from the processed files list, those with full locked regions are added. This is an attempt to harmonize the file handling of the theorem prover and whatever it reports with the scripting inside Proof General. Additionally proof-deactivate-scripting retracts a file with a partly locked region, only the active scripting buffer is allowed such a region (currently).