aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
1998-12-11Tidied output by putting newlines before imports done message.David Aspinall
1998-12-11Fixed bug where proof-activate-scripting nuked locked regions.David Aspinall
1998-12-11Removed proof-send, now use proof-shell-insert instead.David Aspinall
Removed proof-preprocess-input hook function, Paul Callaghan can now use proof-shell-insert-hook instead for his need.
1998-12-11HandyDavid Aspinall
1998-12-11Removed proof-shell-preprocess-command. Improved docstring for ↵David Aspinall
proof-shell-insert-hooks.
1998-12-11Explained one-prover issue better.David Aspinall
1998-12-11. Removed "multiple prover problem" from bugs section, since it's nowDavid Aspinall
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.
1998-12-11Removed multiple provers problem, it's handled gracefully now and not a bug.David Aspinall
1998-12-11Added some items after user feedback. Also some *** probs.David Aspinall
1998-12-11Updated for version 2.0David Aspinall
1998-12-11Disabled span-making part of proof-shell-analyse structure for Emacs 20.3David Aspinall
1998-12-11Added mention of FSFmacs multibyte character problem (version 20.3)David Aspinall
1998-12-10Made point stay at top of goals buffer and bottom of response bufferDavid Aspinall
1998-12-10Changed name of proof-toolbar-inhibit variable for uniformity.David Aspinall
1998-12-10New file mentioning some test cases.David Aspinall
1998-12-10Offer to save script mode buffers which have no files,David Aspinall
in case Emacs is exited accidently. (Esoteric improvement).
1998-12-10Patch for case that new script buffer has no filename.David Aspinall
1998-12-10Fix for splash hack for theory files when proo-splash-inhibit=t.David Aspinall
1998-12-10Fix for proof-splash-inhibit = t. Bug report from Paul Callaghan.David Aspinall
1998-12-08o special characters are no longer displayed in (16Bit) FSF GNU EmacsThomas Kleymann
20.3 o however, there is still a mysterious bug in 'proof-shell-analyse-structure' when processing lego/example.l
1998-12-08Added A*** for documentation, X for ChangeLog in devel distrib.David Aspinall
1998-12-08Added support for proof-shell-restart-cmdThomas Kleymann
1998-12-07Set version tag for new release.David Aspinall
1998-12-07Added proof-shell-preprocess-command for Paul Callaghan.David Aspinall
1998-12-05Added new todos for LEGO.David Aspinall
1998-11-26Set version tag for new release.David Aspinall
1998-11-26Added HTML files.David Aspinall
1998-11-26Added note about final things to do for 2.0David Aspinall
1998-11-26BUG fix: proof-shell-message with str's containing format characters.David Aspinall
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.
1998-11-26Format fixDavid Aspinall
1998-11-26Added clear-goals-buffer stuff, asked for response to be left after use_thy.David Aspinall
1998-11-26Added note about bugs elsewhere. Display issues. Tech rep todosDavid Aspinall
1998-11-26Added proof-shell-clear-goals-regexp.David Aspinall
1998-11-26Warning in proof-shell-insert-hook docstrings.David Aspinall
1998-11-26Quotes added to try to fix markup.David Aspinall
1998-11-26Suggestions for using proof-pre-shell-start-hook removed. Minor typos/fixes.David Aspinall
1998-11-26Alterations to @var case againDavid Aspinall
1998-11-26Improvements from Markus Wenzel. Re-made after texi-docstring-magicDavid Aspinall
1998-11-25Fixup branchDavid Aspinall
1998-11-25Added todo. Put quote into symbol markup.David Aspinall
1998-11-25Added 20.3 version of FSF Emacs and todo for each release.David Aspinall
generated by cgit v1.2.3 (git 2.25.1) at 2026-09-01 00:08:49 +0000