| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 1998-09-03 | Renamed for new subdirectory structure | David Aspinall | |
| 1998-09-03 | Removed dead code | David Aspinall | |
| 1998-08-14 | improved help submenu for LEGO | Thomas Kleymann | |
| - added a link to the library and the reference card for version 1.3 | |||
| 1998-08-07 | o removed log entry | Thomas Kleymann | |
| o changed default for lego-tags o set up regular definitions to support definitions of the form id == term o monitoring the end of imports is now implemented via a new proof-shell-process-output-system-specific hook | |||
| 1998-07-27 | Supports official LEGO release 1.3 | Thomas Kleymann | |
| 1998-06-10 | Added lego-init-syntax-table as function to initialize syntax entries | Healfdene Goguen | |
| particular to LEGO, and call it from lego-shell-mode-config. | |||
| 1998-06-03 | Added '?'s before single characters in define-keys for emacs19, at | Healfdene Goguen | |
| Pascal Brisset's suggestion. | |||
| 1998-06-02 | Generalized proof-retract-target, now parameterized by | Healfdene Goguen | |
| proof-count-undos and proof-find-and-forget. Generalized proof-shell-analyse-structure, introduced variable proof-analyse-using-stack. Generalized proof menu plus ancillary functions. Generalized proof-mode-version-string. Moved various comments into documentation string. | |||
| 1998-05-29 | o outsourced indentation to proof-indent | Thomas Kleymann | |
| o support indentation of commands o replaced test of Emacs version with availability test of specific features o C-c C-c, C-c C-v and M-tab is now available in all buffers | |||
| 1998-05-23 | improved support for Info | Thomas Kleymann | |
| o employed `Info-default-directory-list' rather than `Info-directory-list' so that code also works for Emacs 19.34 o setting of `Info-default-directory-list' now at proof level | |||
| 1998-05-16 | implementation of `lego-shell-adjust-line-width' can now be called as | Thomas Kleymann | |
| part of a hook. This change has been caused by replacing `proof-shell-config' with `proof-shell-insert-hook' | |||
| 1998-05-15 | Changed variable names [s]ext to span. | Healfdene Goguen | |
| 1998-05-12 | Added hook `proof-shell-insert-hook', which is initalized to | Healfdene Goguen | |
| lego-shell-adjust-line-width. This replaces `lego-shell-config'. | |||
| 1998-05-08 | Made separated indentation more elegant. | Healfdene Goguen | |
| Separated consideration of {}'s so it only happens for LEGO. | |||
| 1998-05-08 | Merged indentation code for LEGO and Coq into proof.el. | Healfdene Goguen | |
| 1998-05-06 | Changed lego-undoable-commands-regexp to have "andI" and "andE" | Healfdene Goguen | |
| instead of "AndI" and "AndE". | |||
| 1998-05-06 | Added lego-info-dir so that location of script-management.info can be | Healfdene Goguen | |
| hard-coded. | |||
| 1998-05-05 | Added lego-goal-command-p to fix Coq's problem with "Definition". | Healfdene Goguen | |
| Removed lego-killref from menu. | |||
| 1998-04-27 | removed explicit reference to a binary in ctm's home directory | Thomas Kleymann | |
| 1998-03-25 | added support for etags at generic proof level | Thomas Kleymann | |
| 1998-02-10 | added Dnf to lego-undoable-commands-regexp | Thomas Kleymann | |
| 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 | 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-05 | fixed a bug in the indenting functions | Thomas Kleymann | |
| 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-24 | Added proof-execute-minibuffer-cmd and scripting minor mode. | Dilip Sequiera | |
| 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-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-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-10-24 | New indentation for lego-count-undos (smile) | Healfdene Goguen | |
| 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-13 | lego-count-undos is now aware that comments are treated separately | Thomas Kleymann | |
| 1997-10-08 | *** empty log message *** | Healfdene Goguen | |
| 1997-08-25 | minor change in font-lock pattern | Thomas Kleymann | |
| 1996-12-12 | removed font-lock support for Error messages; this is now supported in | Thomas Kleymann | |
| the pbp package | |||
| 1996-12-09 | Speeded up proof-by-pointing things | Dilip Sequiera | |
| 1996-12-05 | added font-lock properties for pbp-lego-mode | Thomas Kleymann | |
| 1996-12-03 | minor extensions of regular expressions | Thomas Kleymann | |
| 1996-12-03 | Minor fix for performance reasons. | Dilip Sequiera | |
| 1996-12-03 | A few small fixes to deal with performance problems. | Dilip Sequiera | |
| 1996-11-29 | o added logical macros as keywords | Thomas Kleymann | |
| o removed keywords SaveFrozen and SaveUnfrozen o fixed bug in lego-outline-regexp | |||
| 1996-11-22 | *** empty log message *** | Thomas Kleymann | |
| 1996-11-21 | *** empty log message *** | Thomas Kleymann | |
| 1996-11-17 | Cleaned ext.el up a bit in terms of its namespace and the management of | Dilip Sequiera | |
| the comint filter. | |||
| 1996-11-13 | minor changes regarding regular expressions | Thomas Kleymann | |
| 1996-11-13 | Fixed parenthesis matching to deal with comments | Dilip Sequiera | |
| 1996-11-13 | Yves Bertot's proof by pointing | Thomas Kleymann | |
| 1996-11-12 | improved lego-outline-regexp | Thomas Kleymann | |
| 1996-11-10 | fix for incorrect lego-outline-regexp | Thomas Kleymann | |
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |