| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 1999-09-03 | da: improved comment; | Makarius Wenzel | |
| 1999-08-24 | Attempted fix of FSFmacs problem, left as comment | David Aspinall | |
| 1999-08-20 | proof-goto-end-of-locked-if-pos-not-visible-in-window: | David Aspinall | |
| Check that there is active scripting buffer, in Isabelle there might not be. | |||
| 1999-05-27 | improved proof-segment-up-to to support proof-string-start-regexp, | Makarius Wenzel | |
| proof-string-end-regexp; | |||
| 1999-05-25 | proof-done-advancing: added proof-really-save-command-p to support | Makarius Wenzel | |
| more general qed schemes, such as Isabelle/Isar's nested proofs; | |||
| 1999-05-11 | Add toggle for proof toolbar to menu | David Aspinall | |
| 1999-02-22 | Fixed bug by shifting configuration of minor mode for active terminator. | David Aspinall | |
| 1999-02-01 | Used proof-string-match for matching against proof script. | David Aspinall | |
| 1998-12-16 | Removed info file name space, again, arrgggh. | David Aspinall | |
| 1998-12-16 | Added back space in info file name | David Aspinall | |
| 1998-12-16 | Reverted to previous semantics | David Aspinall | |
| 1998-12-16 | Made delete-region arg optional for proof-retract-until-point-interactive. | David Aspinall | |
| 1998-12-16 | Removed space from ProofGeneral name. | David Aspinall | |
| 1998-12-16 | Tweaked docstring for C-c C-u. | David Aspinall | |
| 1998-12-16 | rationalised keybinding (again) | Thomas Kleymann | |
| 1998-12-16 | improved default keybindings | Thomas Kleymann | |
| 1998-12-15 | Docstring fix | David Aspinall | |
| 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. | |||
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |