proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
*	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).
*	Added more commands for testing	David Aspinall	1998-12-11
\|
*	Added submit bug report to proof-shared-menu	David Aspinall	1998-12-11
\|
*	Tweaked headings for bug report	David Aspinall	1998-12-11
\|
*	Added proof-submit-bug-report	David Aspinall	1998-12-11
\|
*	Removed check for proof script buffer from retraction enabler.	David Aspinall	1998-12-11
\|
*	Fixed typo.	David Aspinall	1998-12-11
\|
*	Name of proof-shell-restart was changed.	David Aspinall	1998-12-11
\|
*	Tidied output by putting newlines before imports done message.	David Aspinall	1998-12-11
\|
*	Fixed bug where proof-activate-scripting nuked locked regions.	David Aspinall	1998-12-11
\|
*	Removed proof-send, now use proof-shell-insert instead.	David Aspinall	1998-12-11
\| \| \| \| \|	Removed proof-preprocess-input hook function, Paul Callaghan can now use proof-shell-insert-hook instead for his need.
*	Handy	David Aspinall	1998-12-11
\|
*	Removed proof-shell-preprocess-command. Improved docstring for ↵	David Aspinall	1998-12-11
\| \| \| \|	proof-shell-insert-hooks.
*	Explained one-prover issue better.	David Aspinall	1998-12-11
\|
*	. Removed "multiple prover problem" from bugs section, since it's now	David Aspinall	1998-12-11
\| \| \| \| \| \| \| \|	handled gracefully. It's a limitation rather than a bug per se. . Added a new subsection to Appendix A, for setting names of binaries. . Moved the table of script extensions and mode names to section 1.1 . Added proof-shell-insert and proof-invisible command to Chap 10. . Updated magic.
*	Removed multiple provers problem, it's handled gracefully now and not a bug.	David Aspinall	1998-12-11
\|
*	Added some items after user feedback. Also some *** probs.	David Aspinall	1998-12-11
\|
*	Updated for version 2.0	David Aspinall	1998-12-11
\|
*	Disabled span-making part of proof-shell-analyse structure for Emacs 20.3	David Aspinall	1998-12-11
\|
*	Added mention of FSFmacs multibyte character problem (version 20.3)	David Aspinall	1998-12-11
\|
*	Made point stay at top of goals buffer and bottom of response buffer	David Aspinall	1998-12-10
\|
*	Changed name of proof-toolbar-inhibit variable for uniformity.	David Aspinall	1998-12-10
\|
*	New file mentioning some test cases.	David Aspinall	1998-12-10
\|
*	Offer to save script mode buffers which have no files,	David Aspinall	1998-12-10
\| \| \| \|	in case Emacs is exited accidently. (Esoteric improvement).
*	Patch for case that new script buffer has no filename.	David Aspinall	1998-12-10
\|
*	Fix for splash hack for theory files when proo-splash-inhibit=t.	David Aspinall	1998-12-10
\|
*	Fix for proof-splash-inhibit = t. Bug report from Paul Callaghan.	David Aspinall	1998-12-10
\|
*	o special characters are no longer displayed in (16Bit) FSF GNU Emacs	Thomas Kleymann	1998-12-08
\| \| \| \| \| \| \|	20.3 o however, there is still a mysterious bug in 'proof-shell-analyse-structure' when processing lego/example.l
*	Added A*** for documentation, X for ChangeLog in devel distrib.	David Aspinall	1998-12-08
\|
*	Added support for proof-shell-restart-cmd	Thomas Kleymann	1998-12-08
\|
*	Set version tag for new release.	David Aspinall	1998-12-07
\|
*	Added proof-shell-preprocess-command for Paul Callaghan.	David Aspinall	1998-12-07
\|
*	Added new todos for LEGO.	David Aspinall	1998-12-05
\|
*	Set version tag for new release.	David Aspinall	1998-11-26
\|
*	Added HTML files.	David Aspinall	1998-11-26
\|
*	Added note about final things to do for 2.0	David Aspinall	1998-11-26
\|
*	BUG fix: proof-shell-message with str's containing format characters.	David Aspinall	1998-11-26
\| \| \| \| \| \|	BUG fix: kill-function: another chance to catch process sentinel added. BUG fix: FSF Emacs minor-mode-alist BUG fix: FSF Emacs problem with proof-shell-insert mess. Still probs.
*	Format fix	David Aspinall	1998-11-26
\|