| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 1998-12-18 | Beginnings of x-symbol support. | 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 | 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 | 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 | Disabled span-making part of proof-shell-analyse structure for Emacs 20.3 | David Aspinall | |
| 1998-12-10 | Made point stay at top of goals buffer and bottom of response buffer | David Aspinall | |
| 1998-12-08 | o special characters are no longer displayed in (16Bit) FSF GNU Emacs | Thomas Kleymann | |
| 20.3 o however, there is still a mysterious bug in 'proof-shell-analyse-structure' when processing lego/example.l | |||
| 1998-12-07 | Added proof-shell-preprocess-command for Paul Callaghan. | David Aspinall | |
| 1998-11-26 | BUG fix: proof-shell-message with str's containing format characters. | David Aspinall | |
| BUG fix: kill-function: another chance to catch process sentinel added. BUG fix: FSF Emacs minor-mode-alist BUG fix: FSF Emacs problem with proof-shell-insert mess. Still probs. | |||
| 1998-11-25 | Got rid of an error message in case of process early exiting. | 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 | Improved kill function. Added process sentinel to watch for process exiting. | David Aspinall | |
| 1998-11-25 | Replaced proof-pbp-buffer with proof-goals-buffer. | David Aspinall | |
| 1998-11-25 | In filter: minor improvement for when proof-shell-wakeup-char is set. | David Aspinall | |
| In proof-shell-handle-error: Make action list empty to prevent proof shell filter seeing same error over and over in case user types directly in shell buffer after an error. | |||
| 1998-11-25 | Use make-local-hook instead of make-local-variable | David Aspinall | |
| 1998-11-25 | Fixed up exit hook (still buggy) | David Aspinall | |
| 1998-11-25 | Docstring fixes, minor improvements. | David Aspinall | |
| 1998-11-25 | Improved docstrings | David Aspinall | |
| 1998-11-25 | Docstring fixes | 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 | . Changed behaviour of retracting current scripting buffer: | David Aspinall | |
| now it *nukes* proof-script-buffer-list (possibly unecessarily). Before, current scripting buffer was silently preserved in case it was retracted, but this means that proof-activate-scripting-hook was not run when scripting was begun again in the buffer, which left PG in an inconsistent state with respect to included files (in Isabelle). URGENT: must check this is okay with LEGO. | |||
| 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-12 | Rashly fixed a suspicious looking nested use of set-buffer. Docstrings. | 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-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 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-03 | Being pedantic about variables versus predicates, renamed prog-name-ask-p. | David Aspinall | |
| 1998-11-03 | Removed FIXME | David Aspinall | |
| 1998-11-03 | A* Fix display handling problems (tms, all week) | Thomas Kleymann | |
| Done. :-) | |||
| 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 | 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 | replaced some occurences of (current-buffer) by proof-shell-buffer to | Thomas Kleymann | |
| make code more robust | |||
| 1998-10-29 | Fixed bug in proof-shell-process-urgent-message (preserve point). | David Aspinall | |
| 1998-10-28 | rearranged code to avoid compiler warning messages | Thomas Kleymann | |
| 1998-10-27 | Continuing mods for cleaner byte compile | David Aspinall | |
| 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 | 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 FIXME question about moving point. | David Aspinall | |
| 1998-10-27 | Begun work on clean byte compilation / clarifying interfaces. | David Aspinall | |
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |