| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 1998-05-01 | This commit was generated by cvs2git to track changes on a CVS vendor | David Aspinall | |
| branch. | |||
| 1998-04-27 | removed explicit reference to a binary in ctm's home directory | Thomas Kleymann | |
| 1998-04-17 | X-Symbol version 4.45 beta | David Aspinall | |
| 1998-04-17 | This commit was generated by cvs2git to track changes on a CVS vendor | David Aspinall | |
| branch. | |||
| 1998-04-17 | Version 4.5 (beta?) sent by CW, as a package distrib. | David Aspinall | |
| 1998-04-17 | This commit was generated by cvs2git to track changes on a CVS vendor | David Aspinall | |
| branch. | |||
| 1998-03-25 | added support for etags at generic proof level | Thomas Kleymann | |
| 1998-03-24 | *** empty log message *** | Thomas Kleymann | |
| 1998-02-11 | prioritised | Thomas Kleymann | |
| 1998-02-10 | *** empty log message *** | Thomas Kleymann | |
| 1998-02-10 | added Dnf to lego-undoable-commands-regexp | Thomas Kleymann | |
| 1998-01-26 | X-Symbol version 4.45 beta | David Aspinall | |
| 1998-01-26 | This commit was generated by cvs2git to track changes on a CVS vendor | David Aspinall | |
| branch. | |||
| 1998-01-16 | Commented the code of proof.el and lego.el a bit. Made a minor change | Dilip Sequiera | |
| to the way errors are handled, so that any delayed output is inserted in the buffer before the error message is printed. | |||
| 1998-01-15 | Added coq-shell-cd | Healfdene Goguen | |
| Some new fontlocks | |||
| 1998-01-15 | Updated method of defining proof-shell-cd to be consistent with other | Healfdene Goguen | |
| proof-assistant-dependent variables. Added ctrl-button1 to copy selected region to end of locked region | |||
| 1998-01-15 | One needed change for coq included | Healfdene Goguen | |
| 1998-01-12 | o added support for remote proof processes | Thomas Kleymann | |
| o bound C-c C-z to 'proof-frob-locked-end | |||
| 1998-01-05 | improved fume support | Thomas Kleymann | |
| 1998-01-05 | fixed a bug in the indenting functions | Thomas Kleymann | |
| 1997-12-18 | *** empty log message *** | Thomas Kleymann | |
| 1997-12-18 | o introduced proof-shell-handle-error-hook and bount it by default to | Thomas Kleymann | |
| proof-goto-end-of-locked-if-pos-not-visible-in-window (also new) o proof-find-next-terminator now also works inside a locked region o implemented proof-process-buffer which is by default bount to C-c C-b | |||
| 1997-11-26 | Noted bug in popup-eager-annotation | Dilip Sequiera | |
| 1997-11-26 | Added C-c C-s to run "Search" in Coq. | Healfdene Goguen | |
| Moved coq-goal-with-hole-regexp etc to coq-fontlock. Removed various superfluous definitions for COQPATH etc. | |||
| 1997-11-26 | A few new suggestions | Healfdene Goguen | |
| 1997-11-26 | Incorporated tms's suggestion for simplifying coq-font-lock-keywords-1 | Healfdene Goguen | |
| 1997-11-26 | o The response buffer focusses on the first goal | Thomas Kleymann | |
| o If proof-retract-until-point is is invoked outside a locked region, the last successfully processed command is undone. o Added support for func-menu | |||
| 1997-11-26 | o simplified code: | Thomas Kleymann | |
| lego-goal-with-hole-regexp and lego-save-with-hole-regexp is now used for lego-font-lock-keywords-1 as well o improved lego-find-and-forget | |||
| 1997-11-26 | simplified code: | Thomas Kleymann | |
| lego-goal-with-hole-regexp and lego-save-with-hole-regexp is now used for lego-font-lock-keywords-1 as well | |||
| 1997-11-24 | Added proof-execute-minibuffer-cmd and scripting minor mode. | Dilip Sequiera | |
| 1997-11-20 | Added proof-global-p to test whether a 'vanilla should be lifted above | Healfdene Goguen | |
| active lemmas. Separated proof-lift-global as separate command to lift global declarations above active lemmas. Fixed usual problem that 'cmd is nil for comments in this code. Made lifting globals start from beginning of file rather than go backwards. Fixed bug in pbp code proof-shell-analyse-structure, where stack wasn't cleared for new goal-hyp's. | |||
| 1997-11-20 | Fixed outstanding things to be updated in Coq. | Healfdene Goguen | |
| 1997-11-20 | Added lego-global-p as always false, but for consistency with Coq mode. | Healfdene Goguen | |
| Changed [meta (control i)] to [meta tab] in key definition. | |||
| 1997-11-20 | Added coq-global-p for global declarations and definitions. These now | Healfdene Goguen | |
| get lifted in the same way as lemmas. Changed [meta (control i)] to [meta tab] in key definition. Changed menu, and made help in menu refer to info mode. | |||
| 1997-11-18 | Added indentation for lego-mode. | Dilip Sequiera | |
| 1997-11-17 | Added some magic commands: proof-frob-locked-end, proof-try-command, | Dilip Sequiera | |
| proof-interrupt-process. Added moving nested lemmas above goal for coq. Changed the key mapping for assert-until-point to C-c RET. | |||
| 1997-11-13 | Includes commented code for Coq version of extent protocol | Healfdene Goguen | |
| 1997-11-12 | Changed pbp-change-goal so that it only "Show"s the goal pointed at. | Healfdene Goguen | |
| 1997-11-10 | Started modifications for emacs19 port. | Dilip Sequiera | |
| 1997-11-10 | Put in a workaround for a strange bug in comint which was finding a bunch | Dilip Sequiera | |
| of ^G's from comint-get-old-input for some inexplicable reason. | |||
| 1997-11-06 | Parameterize by proof-goal-hyp-fn in pbp-make-top-extent, to handle | Healfdene Goguen | |
| Coq goals which start with text rather than simply ?n Updated 'let (ap 0)' in proof-shell-analyse structure, to be slightly more compatible with Coq pbp code | |||
| 1997-11-06 | Assign new variable proof-goal-hyp-fn to lego-goal-hyp, which is | Healfdene Goguen | |
| simply old code for picking up goal or hypothesis for pbp | |||
| 1997-11-06 | Assign new variable proof-goal-hyp-fn to coq-goal-hyp, which advances | Healfdene Goguen | |
| over coq-goal-regexp to pick up goal for pbp | |||
| 1997-11-06 | Updates to Coq fontlock tables | Healfdene Goguen | |
| 1997-10-31 | o implented proof-find-next-terminator available via C-c C-e | Thomas Kleymann | |
| o fixed a bug in proof-done-retracting | |||
| 1997-10-30 | Updates for coq, including: | Healfdene Goguen | |
| * pbp-goal-command and pbp-hyp-command use proof-terminal-string * updates to keywords * fix for goal regexp | |||
| 1997-10-24 | Updated comment about extent types | Healfdene Goguen | |
| 1997-10-24 | New indentation for lego-count-undos (smile) | Healfdene Goguen | |
| 1997-10-24 | Fixed coq-count-undos for comments | Healfdene Goguen | |
| 1997-10-24 | Changed order of "Inversion_clear" and "Inversion" so that former is | Healfdene Goguen | |
| fontified first. Added "Print" to list of commands. | |||
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |