aboutsummaryrefslogtreecommitdiff
path: root/generic
AgeCommit message (Collapse)Author
1998-12-15Used authorized keywords.David Aspinall
1998-12-15Docstring fix.David Aspinall
1998-12-15Docstring fixesDavid Aspinall
1998-12-15Docstring fixDavid Aspinall
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-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-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-11Set version tag for new release.David 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-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-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 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-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-11Removed proof-shell-preprocess-command. Improved docstring for ↵David Aspinall
proof-shell-insert-hooks.
1998-12-11Disabled span-making part of proof-shell-analyse structure for Emacs 20.3David 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-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 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-07Set version tag for new release.David Aspinall
1998-12-07Added proof-shell-preprocess-command for Paul Callaghan.David Aspinall
1998-11-26Set version tag for new release.David 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 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-25Added todo. Put quote into symbol markup.David Aspinall
1998-11-25Set version tag for new release.David Aspinall
1998-11-25Got rid of an error message in case of process early exiting.David Aspinall
1998-11-25Docstring improvements.David Aspinall
1998-11-25Documentation improvements.David Aspinall
1998-11-25FSF Emacs fix for buffer-file-truename, which is theDavid Aspinall
*abbreviated* form of file-truename!
1998-11-25Compile clean-ups.David Aspinall
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-22 02:17:08 +0000