| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |
| 1998-10-27 | Removed eval-when-compile around define-derived-mode, it don't work. | David Aspinall | |
| 1998-10-27 | Made handling of multiple files more robust. On changing script | Thomas Kleymann | |
| buffers, we invoke (save-some-buffers). Furthermore, we warn the user if modified buffers have been read in by the proof assistant. | |||
| 1998-10-27 | Fixed up proof-script.el for clean byte compile | David Aspinall | |
| 1998-10-27 | Fix of byte compiler warnings for proof-script.el. | David Aspinall | |
| 1998-10-27 | Moved pbp-goal-command and pbp-hyp-command to proof-config.Moved LEGO specifix. | David Aspinall | |
| 1998-10-27 | Added more comments to proof-activate-scripting | David Aspinall | |
| 1998-10-27 | Removed bug introduced by da trying to do clever optimizations | David Aspinall | |
| 1998-10-27 | Fixed assert-until-point for ignore-process case | David Aspinall | |
| 1998-10-27 | Begun work on clean byte compilation / clarifying interfaces. | David Aspinall | |
| 1998-10-27 | Checked through span code. Commented out dead bits | David Aspinall | |
| 1998-10-27 | Renamed proof-invisible-command proof-shell-invisible-command. | David Aspinall | |
| Removed superfluous optional 'relaxed' argument from: proof-shell-invisibile-command, proof-grab-lock, proof-start-queue. | |||
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |