| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 1999-09-21 | Comment fix. | David Aspinall | |
| Fix for FSF Emacs. | |||
| 1999-09-21 | Robustification so that new instances are easier to add | David Aspinall | |
| (allowed a bunch of regexps to be unset, safely). | |||
| 1999-09-21 | proof-shell-grab-lock runs proof-state-change-hook. | David Aspinall | |
| This results in some flickering of the toolbar (buttons disabled while region is pink), but is The Right Thing. Removed "Inferior" from buffer names. | |||
| 1999-09-21 | Callback for proof-shell-done-invisible now runs proof-state-change-hook. | David Aspinall | |
| 1999-09-13 | Fix so that buffer names are shorter (esp for Coq). | David Aspinall | |
| A fixed version of Patrick's earlier patch. | |||
| 1999-09-09 | tuned x-symbol setup (DvO); | Makarius Wenzel | |
| 1999-08-23 | FIXME to add menu to goals buffer, to match response buffer menu. | David Aspinall | |
| 1999-08-20 | Fix for process kill timeout bug. | David Aspinall | |
| 1999-08-20 | prefer proof-shell-interrupt-regexp over proof-shell-error-regexp | Makarius Wenzel | |
| (interrupts may appear like error messages in Isabelle/Isar); | |||
| 1999-08-20 | Fix for XEmacs 21 | David Aspinall | |
| 1999-07-22 | Reverted change to Inferior buffer's name, it fails on simple | David Aspinall | |
| case of proof-prog-name="isabelle", for example. | |||
| 1999-06-21 | unkillable buffer bugfix | Patrick Loiseleur | |
| 1999-06-14 | Bugfixes in proof-shell-exit and proof-shell-kill-function | Patrick Loiseleur | |
| 1999-06-08 | *** empty log message *** | Patrick Loiseleur | |
| 1999-05-25 | removed superficial space; | Makarius Wenzel | |
| 1999-05-17 | I've added the custom option 'prog-name-guess' in the generic part and | Patrick Loiseleur | |
| the function coq-guess-command-line in the coq part. Every prover should have the functon *-guess-command-line that uses, for example, the output of "make -n" to guess the correct command line options of the prover. Patrick | |||
| 1999-01-15 | Experimental bug fix for Solaris problem | David Aspinall | |
| 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 | |
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |