diff options
| author |  Thomas Kleymann <da+pg-tms@inf.ed.ac.uk> | 1996-11-13 14:47:11 +0000 |
|---|---|---|
| committer | Thomas Kleymann <da+pg-tms@inf.ed.ac.uk> | 1996-11-13 14:47:11 +0000 |
| commit | c4fbc08712cca123931519df890191f01968305f (patch) | |
| tree | c30d799beca9c7414178bf8efbbb7fadcff8eb87 /lego.el | |
| parent | 618504240a2430f899c684a2ed847b40ec3f89c6 (diff) | |
Yves Bertot's proof by pointing
Diffstat (limited to 'lego.el')
| -rw-r--r-- | lego.el | 12 |
1 files changed, 8 insertions, 4 deletions
@@ -4,11 +4,12 @@ ;; code. ;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk> -;; Time-stamp: <12 Nov 96 tms /home/tms/elisp/lego.el> +;; Time-stamp: <13 Nov 96 tms /home/tms/elisp/lego.el> ;; Thanks to David Aspinall, Robert Boyer, Rod Burstall, ;; James McKinna, Mark Ruys, Martin Steffen, Perdita Stevens (require 'proof) +(require 'ext) ; Configuration @@ -24,7 +25,7 @@ is primarily concerned to make life easier. There it will enable pretty printing") -(defconst lego-pretty-on "Configure PrettyOn;" +(defconst lego-pretty-on "Configure PrettyOn; Configure AnnotateOn;" "Command to enable pretty printing of the LEGO process.") (defconst lego-pretty-set-width "Configure PrettyWidth %s;" @@ -111,7 +112,7 @@ (defvar lego-outline-regexp (concat "[[*]\\|" (ids-to-regexp - '("Discharge" "Freeze" "Goal" "Module" "Record" "Inductive" + '("Discharge" "DischargeKeep" "Freeze" "Goal" "Module" "Record" "Inductive" "Unfreeze")))) (defvar lego-outline-heading-end-regexp ";\\|\\*)") @@ -301,8 +302,9 @@ (list (concat "^ \\(" lego-id "\\) = ... :") 1 'font-lock-function-name-face) - (list (concat "^ \\(" lego-id "\\) [:|] ") 1 + (list (concat "^ \\(" lego-id "\\( " lego-id "\\)*\\) [:|] ") 1 'font-lock-declaration-name-face) + ; e.g., decl S1 S2 : prog sort (list (concat "\\<decl\\> \\(" lego-id "\\) [:|]") 1 'font-lock-declaration-name-face) @@ -465,6 +467,8 @@ (setq compilation-search-path (cons nil (lego-get-path))) (add-hook 'proof-safe-send-hook 'lego-adjust-line-width) (add-hook 'proof-shell-exit-hook 'lego-shell-zap-line-width) + (add-hook 'comint-output-filter-functions 'lego-filter t) + (lego-goals-init) (font-lock-fontify-buffer)) |