aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
1998-12-15Updated magic.David Aspinall
1998-12-15Used authorized keywords.David Aspinall
1998-12-15Docstring fix.David Aspinall
1998-12-15Made preface unnumbered. Cosmetic improvements. Updated magic.David Aspinall
1998-12-15Docstring fixesDavid Aspinall
1998-12-15Docstring fixDavid Aspinall
1998-12-15credits now at the beginningThomas Kleymann
1998-12-15Another todo idea added. This version sent to Emacs news groups.David Aspinall
1998-12-15Idea for magical texi-docstring property for symbols to escape auto markup.David Aspinall
1998-12-15Documented markup rules and usage at start of package.David Aspinall
1998-12-15Improved documentation of proof-included-files-list.David Aspinall
1998-12-15*** empty log message ***Thomas Kleymann
1998-12-15Added ps to make all.David Aspinall
1998-12-15Fixed several typos.David Aspinall
Added docstring for proof-deactivate-scripting and mentioned it in Chap 10. Removed spurious mention of defunct function proof-restart-scripting.
1998-12-15Updated magic. Small changes in Chap 11.David Aspinall
1998-12-15Added back magic target, handy to force update of magic.David Aspinall
1998-12-15Removed done stuff. Added LEGO cd hook todo.David Aspinall
1998-12-15radical new version of Credits and References sectionThomas Kleymann
1998-12-15Fixed broken check on proof-mode-hook.David Aspinall
1998-12-15Removed bogus duplicate call of proof-mode-hook at end of proof-config-done.David Aspinall
1998-12-15Fixes for FSF Emacs handling of processes, kill buffer hooks,David Aspinall
and live/dead overlays.
1998-12-15made many minor changes to the documentationThomas Kleymann
1998-12-14Altered order of new para and removed some mailing list addrsDavid Aspinall
1998-12-14Another FSF bug found in the new filter functions, this time for script buffer.David Aspinall
1998-12-14Gave up on buggy Emacs 19 support, now give error for Emacs 19.David Aspinall
1998-12-14Reordered require of cl. Changed deflocal definition.David Aspinall
1998-12-14Log of testing results.David Aspinall
1998-12-14. modified mailing listsThomas Kleymann
. added further benefit in last section
1998-12-14rearrange pages automaticallyThomas Kleymann
1998-12-14fixed bug in lego-shell-adjust-line-width (It now monitors theThomas Kleymann
proof-goals-buffer)
1998-12-14Added section for UITP/TP researchers, mentioning further possibleDavid Aspinall
projects. Added many more mailing list addresses. Not sure what half of them are, need vetting really.
1998-12-11Set version tag for new release.David Aspinall
1998-12-11More comments about multiple file problemsDavid Aspinall
1998-12-11Disabled hack for proof-shell-process-file which allowedDavid Aspinall
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?
1998-12-11CommentsDavid Aspinall
1998-12-11Urgent fix for multiple files wanted.David Aspinall
1998-12-11Allow even the current scripting buffer to be marked atomicallyDavid Aspinall
in case the prover asks it to be. This can happen when loading theory files in Isabelle.
1998-12-11More test cases mentionedDavid Aspinall
1998-12-11todo for Isabelle multiple files.David Aspinall
1998-12-11Altered behaviour to allow retraction part-way through finished scripts.David Aspinall
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).
1998-12-11Added new test/comments.David Aspinall
1998-12-11UpdatesDavid Aspinall
1998-12-11Several changes:David Aspinall
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).
1998-12-11Added more commands for testingDavid Aspinall
1998-12-11Added submit bug report to proof-shared-menuDavid Aspinall
1998-12-11Tweaked headings for bug reportDavid Aspinall
1998-12-11Added proof-submit-bug-reportDavid Aspinall
1998-12-11Removed check for proof script buffer from retraction enabler.David Aspinall
1998-12-11Fixed typo.David Aspinall
1998-12-11Name of proof-shell-restart was changed.David Aspinall
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 04:01:04 +0000