| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 1998-12-18 | Beginnings of x-symbol support. | David Aspinall | |
| 1998-12-18 | Added proof-assistant-symbol | David Aspinall | |
| 1998-12-17 | Set version tag for new release. | David Aspinall | |
| 1998-12-17 | Set version tag for new release. | David Aspinall | |
| 1998-12-17 | Set version tag for new release. | David Aspinall | |
| 1998-12-17 | Updated docstring. | David Aspinall | |
| 1998-12-17 | Removed a todo. This version submitted for Texinfo. | David Aspinall | |
| 1998-12-17 | Newline after first sentence. Submitted for Texinfo distribution. | David Aspinall | |
| 1998-12-16 | Set version tag for new release. | 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 | Set version tag for new release. | 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 | Set version tag for new release. | Thomas Kleymann | |
| 1998-12-16 | Set version tag for new release. | Thomas Kleymann | |
| 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-16 | Added GPL license (I wrote this at home). | David Aspinall | |
| Corrected name of Texinfo and other comments. | |||
| 1998-12-16 | Fixed default for proof-shell-quit-cmd. | David Aspinall | |
| 1998-12-15 | Set version tag for new release. | David Aspinall | |
| 1998-12-15 | Used authorized keywords. | David Aspinall | |
| 1998-12-15 | Docstring fix. | David Aspinall | |
| 1998-12-15 | Docstring fixes | David Aspinall | |
| 1998-12-15 | Docstring fix | David Aspinall | |
| 1998-12-15 | Another todo idea added. This version sent to Emacs news groups. | David Aspinall | |
| 1998-12-15 | Idea for magical texi-docstring property for symbols to escape auto markup. | David Aspinall | |
| 1998-12-15 | Documented markup rules and usage at start of package. | David Aspinall | |
| 1998-12-15 | Improved documentation of proof-included-files-list. | 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-14 | Gave up on buggy Emacs 19 support, now give error for Emacs 19. | David Aspinall | |
| 1998-12-14 | Reordered require of cl. Changed deflocal definition. | David Aspinall | |
| 1998-12-11 | Set version tag for new release. | David Aspinall | |
| 1998-12-11 | Disabled hack for proof-shell-process-file which allowed | David 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-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 | 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 | |
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |