| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | Improved proof-clean-buffer. Now only deletes windows in currently | David Aspinall | |
| selected frame. Changed default proof-auto-delete-windows value back to t. | |||
| 1998-11-18 | improvements to docstrings and defcustoms. | David Aspinall | |
| added proof-shell-clear-response-regexp | |||
| 1998-11-18 | Bug fix and adjustments in proof-response-buffer-display | David Aspinall | |
| 1998-11-18 | Removed proof-response-buffer-display from byte compile autoloads | David Aspinall | |
| 1998-11-18 | . bug fix for proof-shell-live-buffer. | David Aspinall | |
| . bug fix for proof-shell-filter for case that prompt isn't seen in first output chunk. . bug fix of handling urgent messages in delayed output: skip past the last one seen. Previously messages were put into the response buffer *twice* (first time highlighted). Don't clear the response buffer between urgent messages and delayed output within the same prompt-delimited region. . big improvement of display handling for response buffer, via new function proof-shell-maybe-erase-response. . added proof-shell-clear-response-regexp . docstring fixes. | |||
| 1998-11-18 | Added optional argument to proof-ids for non-comma separators. | 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 | Rashly fixed a suspicious looking nested use of set-buffer. Docstrings. | David Aspinall | |
| 1998-11-12 | Added proof-auto-delete-windows user option. | 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 | Set version tag for new release. | David Aspinall | |
| 1998-11-10 | Added buffers menu, and added shared menu to shell and response buffers. | David Aspinall | |
| 1998-11-10 | Removed references of proof-shell-noise-regexp | Thomas Kleymann | |
| 1998-11-10 | Fixed bug for when proof-rsh-command is empty | David Aspinall | |
| 1998-11-10 | Refresh response buffer when goals buffer is refreshed. | Thomas Kleymann | |
| 1998-11-09 | Added docstring | David Aspinall | |
| 1998-11-09 | Added proof-rsh-command to help complete documentation (was allocated | David Aspinall | |
| to tms but he said he wouldn't get around to it) | |||
| 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-09 | Added acknowledgements to doc. Removed from code. | David Aspinall | |
| 1998-11-06 | (Failed) Attempt to recognize XEmacs with broken jpeg support | David Aspinall | |
| 1998-11-06 | Give error message when attempting to load a second instance of Proof | David Aspinall | |
| General, and give up loading. To save embarrasment in demos, 8-). | |||
| 1998-11-04 | Set version tag for new release. | David Aspinall | |
| 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 | Removed FIXME | David Aspinall | |
| 1998-11-03 | Customization group and type fixes | David Aspinall | |
| 1998-11-03 | Func menu problems, note added | David Aspinall | |
| 1998-11-03 | Note added. | David Aspinall | |
| 1998-11-03 | Improved docstrings | David Aspinall | |
| 1998-11-03 | added FIXME note on maybe using regexp-opt | David Aspinall | |
| 1998-11-03 | Added menu made from toolbar commands, called "Scripting". | David Aspinall | |
| Made file FSF GNU Emacs compatible. | |||
| 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-03 | Promoted proof-window-dedicated to be a user option, and | David Aspinall | |
| renamed it [to reserve -p only for functions (predicates)]. | |||
| 1998-11-03 | Set version tag for new release. | Thomas Kleymann | |
| 1998-11-03 | fixed bug with font-lock face names | Thomas Kleymann | |
| 1998-11-03 | A* Fix display handling problems (tms, all week) | Thomas Kleymann | |
| Done. :-) | |||
| 1998-11-02 | Proof General no longer moves point in the current-buffer | Thomas Kleymann | |
| 1998-11-02 | Quick fix for multiple file problem when current scripting buffer is ↵ | David Aspinall | |
| retracted by prover. | |||
| 1998-11-02 | Proof General no longer changes selected window/buffer under your feet. | Thomas Kleymann | |
| 1998-11-02 | Set version tag for new release. | Thomas Kleymann | |
| 1998-11-02 | fixed minor bugs | Thomas Kleymann | |
| 1998-11-01 | o added support for byte-compilation | Thomas Kleymann | |
| o removed hhg tags in todo o fixed font-lock for FSF Emacs 20.2 o ensured that goals buffer is updated for longer queues o fixed a bug in proof-universal-keys-only-mode | |||
| 1998-10-30 | implemented new buffer model. The goals buffer is now exclusively | Thomas Kleymann | |
| reserved for goals. | |||
| 1998-10-30 | Set version tag for new release. | Thomas Kleymann | |
| 1998-10-30 | replaced some occurences of (current-buffer) by proof-shell-buffer to | Thomas Kleymann | |
| make code more robust | |||
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |