| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 1998-12-11 | Allow even the current scripting buffer to be marked atomically | David Aspinall | |
| in case the prover asks it to be. This can happen when loading theory files in Isabelle. | |||
| 1998-12-11 | Several 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-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 | 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 | |
| Removed proof-preprocess-input hook function, Paul Callaghan can now use proof-shell-insert-hook instead for his need. | |||
| 1998-12-11 | Removed proof-shell-preprocess-command. Improved docstring for ↵ | David Aspinall | |
| proof-shell-insert-hooks. | |||
| 1998-12-11 | Disabled span-making part of proof-shell-analyse structure for Emacs 20.3 | David Aspinall | |
| 1998-12-10 | 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 | Offer to save script mode buffers which have no files, | David Aspinall | |
| in case Emacs is exited accidently. (Esoteric improvement). | |||
| 1998-12-10 | Patch for case that new script buffer has no filename. | David Aspinall | |
| 1998-12-10 | Fix for proof-splash-inhibit = t. Bug report from Paul Callaghan. | David Aspinall | |
| 1998-12-08 | o special characters are no longer displayed in (16Bit) FSF GNU Emacs | Thomas Kleymann | |
| 20.3 o however, there is still a mysterious bug in 'proof-shell-analyse-structure' when processing lego/example.l | |||
| 1998-12-07 | Set version tag for new release. | David Aspinall | |
| 1998-12-07 | Added proof-shell-preprocess-command for Paul Callaghan. | David Aspinall | |
| 1998-11-26 | Set version tag for new release. | David Aspinall | |
| 1998-11-26 | BUG 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-26 | Format fix | David Aspinall | |
| 1998-11-26 | Added proof-shell-clear-goals-regexp. | David Aspinall | |
| 1998-11-26 | Warning in proof-shell-insert-hook docstrings. | David Aspinall | |
| 1998-11-26 | Quotes added to try to fix markup. | David Aspinall | |
| 1998-11-26 | Suggestions for using proof-pre-shell-start-hook removed. Minor typos/fixes. | David Aspinall | |
| 1998-11-26 | Alterations to @var case again | David Aspinall | |
| 1998-11-25 | Added todo. Put quote into symbol markup. | David Aspinall | |
| 1998-11-25 | Set version tag for new release. | David Aspinall | |
| 1998-11-25 | Got rid of an error message in case of process early exiting. | David Aspinall | |
| 1998-11-25 | Docstring improvements. | David Aspinall | |
| 1998-11-25 | Documentation improvements. | David Aspinall | |
| 1998-11-25 | FSF Emacs fix for buffer-file-truename, which is the | David Aspinall | |
| *abbreviated* form of file-truename! | |||
| 1998-11-25 | Compile clean-ups. | David Aspinall | |
| 1998-11-25 | Improved kill function. Added process sentinel to watch for process exiting. | David Aspinall | |
| 1998-11-25 | Replaced proof-pbp-buffer with proof-goals-buffer. | David Aspinall | |
| 1998-11-25 | Rearranged order of regexps, added *emphasised* markup case. | David Aspinall | |
| 1998-11-25 | Note about window dedicated problem. | David Aspinall | |
| 1998-11-25 | Added "start proof assistant" menu option | David Aspinall | |
| 1998-11-25 | Toolbar tip for restart changed. | David Aspinall | |
| 1998-11-25 | In filter: minor improvement for when proof-shell-wakeup-char is set. | David Aspinall | |
| In proof-shell-handle-error: Make action list empty to prevent proof shell filter seeing same error over and over in case user types directly in shell buffer after an error. | |||
| 1998-11-25 | Docstring improvements. | David Aspinall | |
| Made default for proof-window-dedicated be nil because of problems with multi frame stuff. | |||
| 1998-11-25 | Use make-local-hook instead of make-local-variable | David Aspinall | |
| 1998-11-25 | Made default proof-auto-delete-windows=nil again, it's too unpredictable. | David Aspinall | |
| 1998-11-25 | fixed up newlines in @lisp environments. | David Aspinall | |
| 1998-11-25 | Fixed up exit hook (still buggy) | David Aspinall | |
| 1998-11-25 | Improved error handling in proof-deactivate-scripting since | David Aspinall | |
| it's used in a kill hook. | |||
| 1998-11-25 | Docstring fixes, minor improvements. | David Aspinall | |
| 1998-11-25 | more improvements, docstring fixes. | David Aspinall | |
| 1998-11-25 | Wrote proof-deactiveate-scripting command for turning off scripting | David Aspinall | |
| in the current buffer, automatically. Improved kill buffer hook for script buffers. Docstring fixes. | |||
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |