| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 1998-08-21 | First attempt, proof state works. | David Aspinall | |
| 1998-08-21 | Added comments. Made wakeup-char an option. | David Aspinall | |
| 1998-08-21 | Typos and fixes in Walkthrough section. | David Aspinall | |
| 1998-08-21 | Info file is easily generated from texinfo, so doesn't belong in CVS | David Aspinall | |
| 1998-08-21 | todo | 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-14 | *** empty log message *** | Thomas Kleymann | |
| 1998-08-14 | *** empty log message *** | Thomas Kleymann | |
| 1998-08-14 | supports definitions of the form id == foo; | Thomas Kleymann | |
| 1998-08-11 | New branch | David Aspinall | |
| 1998-08-11 | Isabelle proof.el support. | David Aspinall | |
| 1998-08-11 | Renamed <file>-fontlock to <file>-syntax | David Aspinall | |
| 1998-08-07 | *** empty log message *** | Thomas Kleymann | |
| 1998-08-07 | o removed log entry | Thomas Kleymann | |
| o monitoring the end of imports is now implemented via a new proof-shell-process-output-system-specific hook | |||
| 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-08-07 | *** empty log message *** | Thomas Kleymann | |
| 1998-07-27 | Supports official LEGO release 1.3 | Thomas Kleymann | |
| 1998-06-11 | Moved proof-mode-hooks from proof-shell-config-done to | Healfdene Goguen | |
| proof-config-done. | |||
| 1998-06-11 | Added "Scheme" as definition keyword. | Healfdene Goguen | |
| 1998-06-10 | Wrote generic span functions for making spans read-only or read-write. | Healfdene Goguen | |
| Fixed bug in add-span and remove-span concerning return value of span-traverse. | |||
| 1998-06-10 | Wrote generic span functions for making spans read-only or read-write. | Healfdene Goguen | |
| 1998-06-10 | In proof-init-segmentation, only create proof-queue-span and | Healfdene Goguen | |
| proof-locked-span if they don't already exist. Call generic span function for making spans read-only. | |||
| 1998-06-10 | Compare span-end first rather than span-start in span-lt, because | Healfdene Goguen | |
| proof-lock-span is often changed and has starting point 1. Factored out common code of add-span and remove-span into span-traverse. | |||
| 1998-06-10 | Added proof-unprocessed-begin as general function to find beginning of | Healfdene Goguen | |
| unprocessed region. This should be used instead of proof-locked-end if we're not guaranteed to be in scripting buffer. proof-locked-end now calls proof-unprocessed-begin if we're in the proof-script-buffer. We set the goal name to "Unnamed_thm" if we can't find any other name for the theorem. proof-process-active-terminator now calls proof-unprocessed-begin. proof-shell-config-done now calls 'proof-mode-hook. | |||
| 1998-06-10 | Changed "\\s " to "\\s-" in proof-id as whitespace pattern. | Healfdene Goguen | |
| 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-10 | Added coq-init-syntax-table as function to initialize syntax entries | Healfdene Goguen | |
| particular to coq. Changed proof-ctxt-string to "Print All". Call coq-init-syntax-table from coq-shell-mode-config. This was necessary to get prompts with "'"s in them (coming from goals with same) recognized. | |||
| 1998-06-10 | Added "Mutual Inductive" as definition keyword. | Healfdene Goguen | |
| Changed "\\s " into "\\s-" as whitespace pattern. | |||
| 1998-06-09 | o fixed bug in setting proof-queue-face on a colour terminal for GNU | Thomas Kleymann | |
| Emacs (19.34) o adjusting the directory (at least for LEGO) must not contain "~". We now expand `default-directory' before cding to it. [Under XEmacs (unlike Emacs 19.34), `default-directory' is already in expanded form.] | |||
| 1998-06-03 | Added '?'s before single characters in define-keys for emacs19, at | Healfdene Goguen | |
| Pascal Brisset's suggestion. | |||
| 1998-06-03 | Changed Compute from command to tactic. | Healfdene Goguen | |
| Added Fix, Destruct and Cofix as tactics. Added Local as goal. | |||
| 1998-06-03 | Changed last-span to before-list. | Healfdene Goguen | |
| Added definitions of foldr and foldl if they aren't already loaded. Changed definitions of add-span, remove-span and find-span-aux to be non-recursive. Removed detach-extent since this file isn't used by xemacs. Added function append-unique to avoid repetitions in list generated by spans-at-region. Changed next-span so it uses member-if. | |||
| 1998-06-03 | Added (require 'cl) for emacs19. | Healfdene Goguen | |
| 1998-06-03 | Added proof-goto-end-of-locked-interactive as old | Healfdene Goguen | |
| proof-goto-end-of-locked, and proof-goto-end-of-locked now doesn't switch buffer. Added code in proof-steal-process to handle case of stealing script management from a killed buffer. Set proof-active-buffer-fake-minor-mode to nil in proof-restart-script. | |||
| 1998-06-03 | Changed expression (>= 0 x) to its equivalent (eq x 0) | Healfdene Goguen | |
| Changed some variables to their associated constant in cases where we know they must be equal. | |||
| 1998-06-03 | Added definition of proof-commands-regexp for coq | Healfdene Goguen | |
| 1998-06-02 | Structured review now done. | Healfdene Goguen | |
| Added item that we need to write proof-retract-file. | |||
| 1998-06-02 | Corrected comment about this being for emacs19. | Healfdene Goguen | |
| 1998-06-02 | Corrected comment about this being for xemacs. | Healfdene Goguen | |
| 1998-06-02 | Added comment about C-c ' that it will switch to the scripting buffer. | Healfdene Goguen | |
| 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. Removed emacs-version-at-least. Removed comment about buffer-display-table. Moved various comments into documentation string. Fixed another mode-line command for emacs19. | |||
| 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-06-02 | Minor modifications to comments | Healfdene Goguen | |
| 1998-05-29 | fixed a bug in `proof-goto-end-of-locked-if-pos-not-visible-in-window' | Thomas Kleymann | |
| 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-26 | Necessary changes for emacs19 version | Healfdene Goguen | |
| 1998-05-26 | Removed commented code in proof-dont-show-annotations | Healfdene Goguen | |
| proof-done-trying deletes the spans that were created | |||
| 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-22 | Correct path for coq-prog-name and coq-tags. | Healfdene Goguen | |
| 1998-05-22 | fixed a bug in proof-frob-locked-end | Thomas Kleymann | |
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |