| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 1998-12-15 | Removed bogus duplicate call of proof-mode-hook at end of proof-config-done. | David Aspinall | |
| 1998-12-15 | Fixes for FSF Emacs handling of processes, kill buffer hooks, | David Aspinall | |
| and live/dead overlays. | |||
| 1998-12-15 | made many minor changes to the documentation | Thomas Kleymann | |
| 1998-12-11 | Comments | David Aspinall | |
| 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 | Fixed typo. | David Aspinall | |
| 1998-12-11 | Fixed bug where proof-activate-scripting nuked locked regions. | 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-11-25 | Docstring 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 | Replaced proof-pbp-buffer with proof-goals-buffer. | David Aspinall | |
| 1998-11-25 | Added "start proof assistant" menu option | David Aspinall | |
| 1998-11-25 | Use make-local-hook instead of make-local-variable | 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 | 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. | |||
| 1998-11-25 | Improved docstrings | David Aspinall | |
| 1998-11-25 | Docstring fixes | David Aspinall | |
| 1998-11-20 | Minor cleanups | David Aspinall | |
| 1998-11-20 | Reimplemented functions to shut down and restart proof process. | David Aspinall | |
| Scrapped proof-shell-exit-hook. Added proof-shell-quit-cmdd, proof-shell-restart-comd Fancier Scripting indicator for active scripting buffer. | |||
| 1998-11-20 | BIG CHANGES -- SORRY! | David Aspinall | |
| Replaced proof-script-buffer-list with proof-script-buffer. The list was causing too much confusion and nasty bugs used with Isabelle multiple files. Implemented proof-script-buffers and proof-restart-all-buffers, other functions. | |||
| 1998-11-18 | proof-done-retracting: changed delete-region to kill-region after | David Aspinall | |
| Martin Hofmann's suggestion. | |||
| 1998-11-18 | Bug fix: proof-undo-last-successful-command has silent failure for | David Aspinall | |
| empty locked region. | |||
| 1998-11-18 | . Bug fix: moved proof-mark-buffer-atomic from proof-mode body to | David Aspinall | |
| proof-config-done, since it relies on some configuration being set! . Removed test for script buffer in proof-unprocessed-begin to allow non-script buffers to be properly recognized as being locked. . Proof restart script now works on all included files, not just those in the proof-script-buffer-list. This means non script buffers are correctly unlocked when scripting is restarted. . Bug fix in proof-register-possibly-new-processed-file to mark buffer atomic according to the comment (previously failed if proof-script-buffer-list happened to be empty) . Bug fix so proof-undo-last-successful-command fails silently on buffer without locked regions. | |||
| 1998-11-18 | Removed proof-response-buffer-display from byte compile autoloads | David Aspinall | |
| 1998-11-12 | In a fit of autocracy, removed proof-tags-support, binding for | David Aspinall | |
| M-tab and appearance of Find Tags in PG menu. The menu entry already appears in Tools->Tags, and users should bind M-tab for themselves. | |||
| 1998-11-12 | Added Goals buffer to buffers menu -- I forgot it\! | David Aspinall | |
| 1998-11-12 | Minor improvement to atrocious performance of proof-sement-up-to. | David Aspinall | |
| 1998-11-12 | Fixed bug with find-next-terminator. | David Aspinall | |
| 1998-11-12 | Renamed proof-mode-name -> proof-general-name. | David Aspinall | |
| Reimplemented configuration for fume-menu. Now works for named goals, named saves, and (e.g. lego) both! Removed some FIXME's. | |||
| 1998-11-10 | Added buffers menu, and added shared menu to shell and response buffers. | David Aspinall | |
| 1998-11-09 | Added docstring | David Aspinall | |
| 1998-11-09 | Added proof-script-indent user option, to enable indentation code. | David Aspinall | |
| Disabled by default. May be activated by particular proof assistants if they feel confident about it. I don't. Made proof-indent be autoloaded as needed. Lets pray it won't be. | |||
| 1998-11-09 | Added proof-strict-read-only, probably a handy new user-option. | David Aspinall | |
| Side effect is that it's default value of nil for FSF Emacs avoids the font lock problem with span-read-only for FSF Emacs. XEmacs does not have the warning message implemented yet. | |||
| 1998-11-03 | Being pedantic about variables versus predicates, renamed prog-name-ask-p. | David Aspinall | |
| 1998-11-03 | Added docstring | David Aspinall | |
| 1998-11-03 | Func menu problems, note added | David Aspinall | |
| 1998-11-03 | Note added. | David Aspinall | |
| 1998-11-03 | Renamed a couple of menu functions in case of later making | David Aspinall | |
| proof-menu.el. Always call proof-toolbar-setup. | |||
| 1998-11-02 | Quick fix for multiple file problem when current scripting buffer is ↵ | David Aspinall | |
| retracted by prover. | |||
| 1998-10-30 | implemented new buffer model. The goals buffer is now exclusively | Thomas Kleymann | |
| reserved for goals. | |||
| 1998-10-30 | replaced some occurences of (current-buffer) by proof-shell-buffer to | Thomas Kleymann | |
| make code more robust | |||
| 1998-10-29 | More hacks to variable names for customize (sorry) | David Aspinall | |
| 1998-10-29 | Fixed requires for FSF Emacs. | David Aspinall | |
| Patched (old bug?) in proof-response-buffer-display, how did it come back? | |||
| 1998-10-28 | Added proof-toolbar-follow-mode user option and functions to support | David Aspinall | |
| it. Removed require on proof-shell from proof-toolbar. | |||
| 1998-10-28 | rearranged code to avoid compiler warning messages | Thomas Kleymann | |
| 1998-10-27 | More fixes for cleaner byte compile. | David Aspinall | |
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |