| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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. | |||
| 1997-10-22 | Updated proof-segment-up-to to take ""'s into account | Healfdene Goguen | |
| Hence, << Cd "../x". >> works in Coq, and << echo "hello; world"; >> should work in LEGO But maybe we don't want "Cd"'s at all... | |||
| 1997-10-17 | proof-active-terminator inside comment case fixed. Also maybe the | Dilip Sequiera | |
| continuous pbp-buffer update bug. | |||
| 1997-10-17 | Fixed coq-shell-prompt-pattern to reflect proof-id | Healfdene Goguen | |
| Changed ";" to "." in coq-save-with-hole-regexp New modifications to syntax table to reflect actual use of symbols in Coq | |||
| 1997-10-17 | Added "Induction" as tactic | Healfdene Goguen | |
| 1997-10-17 | fixed a bug in proof-process-active-terminator. Notice that it still | Thomas Kleymann | |
| doesn't work when you are inside a comment and press the proof-terminal-char | |||
| 1997-10-16 | Figured out display tables. | Dilip Sequiera | |
| 1997-10-16 | Merged Coq changes with main branch. | Dilip Sequiera | |
| 1997-10-16 | Merged Coq changes onto main branch | Dilip Sequiera | |
| 1997-10-16 | merged script management (1.10.2.18) with main branch | Thomas Kleymann | |
| 1997-10-16 | o merged script management (1.20.2.11) on the main branch | Thomas Kleymann | |
| o fixed a bug in lego-find-and-forget due to new treatment of comments | |||
| 1997-10-14 | proof-process-active-terminator is now an extension of | Thomas Kleymann | |
| proof-assert-until-point (it was broken and looks healthier now) | |||
| 1997-10-13 | *** empty log message *** | Thomas Kleymann | |
| 1997-10-13 | put script-management branch back on main branch | Thomas Kleymann | |
| 1997-10-13 | The package pbp is now integrated in the proof package | Thomas Kleymann | |
| 1997-10-13 | lego-count-undos is now aware that comments are treated separately | Thomas Kleymann | |
| 1997-10-08 | *** empty log message *** | Healfdene Goguen | |
| 1997-09-18 | X-Symbol version 4.45 beta | David Aspinall | |
| 1997-09-18 | This commit was generated by cvs2git to track changes on a CVS vendor | David Aspinall | |
| branch. | |||
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |