Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | One needed change for coq included | 1998-01-15 | |
| | |||
* | o added support for remote proof processes | 1998-01-12 | |
| | | | | o bound C-c C-z to 'proof-frob-locked-end | ||
* | improved fume support | 1998-01-05 | |
| | |||
* | fixed a bug in the indenting functions | 1998-01-05 | |
| | |||
* | *** empty log message *** | 1997-12-18 | |
| | |||
* | o introduced proof-shell-handle-error-hook and bount it by default to | 1997-12-18 | |
| | | | | | | | | 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 | ||
* | Noted bug in popup-eager-annotation | 1997-11-26 | |
| | |||
* | Added C-c C-s to run "Search" in Coq. | 1997-11-26 | |
| | | | | | Moved coq-goal-with-hole-regexp etc to coq-fontlock. Removed various superfluous definitions for COQPATH etc. | ||
* | A few new suggestions | 1997-11-26 | |
| | |||
* | Incorporated tms's suggestion for simplifying coq-font-lock-keywords-1 | 1997-11-26 | |
| | |||
* | o The response buffer focusses on the first goal | 1997-11-26 | |
| | | | | | | 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 | ||
* | o simplified code: | 1997-11-26 | |
| | | | | | | 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 | ||
* | simplified code: | 1997-11-26 | |
| | | | | | lego-goal-with-hole-regexp and lego-save-with-hole-regexp is now used for lego-font-lock-keywords-1 as well | ||
* | Added proof-execute-minibuffer-cmd and scripting minor mode. | 1997-11-24 | |
| | |||
* | Added proof-global-p to test whether a 'vanilla should be lifted above | 1997-11-20 | |
| | | | | | | | | | | | 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. | ||
* | Fixed outstanding things to be updated in Coq. | 1997-11-20 | |
| | |||
* | Added lego-global-p as always false, but for consistency with Coq mode. | 1997-11-20 | |
| | | | | Changed [meta (control i)] to [meta tab] in key definition. | ||
* | Added coq-global-p for global declarations and definitions. These now | 1997-11-20 | |
| | | | | | | 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. | ||
* | Added indentation for lego-mode. | 1997-11-18 | |
| | |||
* | Added some magic commands: proof-frob-locked-end, proof-try-command, | 1997-11-17 | |
| | | | | | proof-interrupt-process. Added moving nested lemmas above goal for coq. Changed the key mapping for assert-until-point to C-c RET. | ||
* | Includes commented code for Coq version of extent protocol | 1997-11-13 | |
| | |||
* | Changed pbp-change-goal so that it only "Show"s the goal pointed at. | 1997-11-12 | |
| | |||
* | Started modifications for emacs19 port. | 1997-11-10 | |
| | |||
* | Put in a workaround for a strange bug in comint which was finding a bunch | 1997-11-10 | |
| | | | | of ^G's from comint-get-old-input for some inexplicable reason. | ||
* | Parameterize by proof-goal-hyp-fn in pbp-make-top-extent, to handle | 1997-11-06 | |
| | | | | | | | 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 | ||
* | Assign new variable proof-goal-hyp-fn to lego-goal-hyp, which is | 1997-11-06 | |
| | | | | simply old code for picking up goal or hypothesis for pbp | ||
* | Assign new variable proof-goal-hyp-fn to coq-goal-hyp, which advances | 1997-11-06 | |
| | | | | over coq-goal-regexp to pick up goal for pbp | ||
* | Updates to Coq fontlock tables | 1997-11-06 | |
| | |||
* | o implented proof-find-next-terminator available via C-c C-e | 1997-10-31 | |
| | | | | o fixed a bug in proof-done-retracting | ||
* | Updates for coq, including: | 1997-10-30 | |
| | | | | | | * pbp-goal-command and pbp-hyp-command use proof-terminal-string * updates to keywords * fix for goal regexp | ||
* | Updated comment about extent types | 1997-10-24 | |
| | |||
* | New indentation for lego-count-undos (smile) | 1997-10-24 | |
| | |||
* | Fixed coq-count-undos for comments | 1997-10-24 | |
| | |||
* | Changed order of "Inversion_clear" and "Inversion" so that former is | 1997-10-24 | |
| | | | | | fontified first. Added "Print" to list of commands. | ||
* | Updated proof-segment-up-to to take ""'s into account | 1997-10-22 | |
| | | | | | | Hence, << Cd "../x". >> works in Coq, and << echo "hello; world"; >> should work in LEGO But maybe we don't want "Cd"'s at all... | ||
* | proof-active-terminator inside comment case fixed. Also maybe the | 1997-10-17 | |
| | | | | continuous pbp-buffer update bug. | ||
* | Fixed coq-shell-prompt-pattern to reflect proof-id | 1997-10-17 | |
| | | | | | Changed ";" to "." in coq-save-with-hole-regexp New modifications to syntax table to reflect actual use of symbols in Coq | ||
* | Added "Induction" as tactic | 1997-10-17 | |
| | |||
* | fixed a bug in proof-process-active-terminator. Notice that it still | 1997-10-17 | |
| | | | | | doesn't work when you are inside a comment and press the proof-terminal-char | ||
* | Figured out display tables. | 1997-10-16 | |
| | |||
* | Merged Coq changes with main branch. | 1997-10-16 | |
| | |||
* | Merged Coq changes onto main branch | 1997-10-16 | |
| | |||
* | merged script management (1.10.2.18) with main branch | 1997-10-16 | |
| | |||
* | o merged script management (1.20.2.11) on the main branch | 1997-10-16 | |
| | | | | o fixed a bug in lego-find-and-forget due to new treatment of comments | ||
* | proof-process-active-terminator is now an extension of | 1997-10-14 | |
| | | | | proof-assert-until-point (it was broken and looks healthier now) | ||
* | *** empty log message *** | 1997-10-13 | |
| | |||
* | put script-management branch back on main branch | 1997-10-13 | |
| | |||
* | The package pbp is now integrated in the proof package | 1997-10-13 | |
| | |||
* | lego-count-undos is now aware that comments are treated separately | 1997-10-13 | |
| | |||
* | *** empty log message *** | 1997-10-08 | |
| |