diff options
author | Thomas Kleymann <da+pg-tms@inf.ed.ac.uk> | 1998-10-30 16:34:38 +0000 |
---|---|---|
committer | Thomas Kleymann <da+pg-tms@inf.ed.ac.uk> | 1998-10-30 16:34:38 +0000 |
commit | 00c337af2ea574baf01a26581b80aa1fd955e2f0 (patch) | |
tree | bc522ddcd85ecae4f3db4fc007dc22b771d9591c /lego/lego.el | |
parent | 4159c005b516ea482b6d0e5fc5e1d960348383c4 (diff) |
implemented new buffer model. The goals buffer is now exclusively
reserved for goals.
Diffstat (limited to 'lego/lego.el')
-rw-r--r-- | lego/lego.el | 26 |
1 files changed, 19 insertions, 7 deletions
diff --git a/lego/lego.el b/lego/lego.el index 869cf50a..3674979d 100644 --- a/lego/lego.el +++ b/lego/lego.el @@ -10,6 +10,8 @@ ;; (require 'proof) +(require 'proof-script) +(require 'proof-shell) (require 'lego-syntax) ;; FIXME: outline should be autoloaded @@ -178,10 +180,17 @@ (easy-menu-change (list proof-mode-name) (car proof-help-menu) (append (cdr proof-help-menu) lego-help-menu-list))) +(eval-and-compile + (define-derived-mode lego-response-mode proof-response-mode + "LEGOResp" nil + (setq font-lock-keywords lego-font-lock-terms) + (proof-response-config-done))) + (define-derived-mode lego-pbp-mode pbp-mode - "pbp" nil + "LEGOGoals" "LEGO Proof State" (lego-pbp-mode-config)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Code that's lego specific ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -354,9 +363,10 @@ ))))) (defun lego-pre-shell-start () - (setq proof-prog-name lego-prog-name) - (setq proof-mode-for-shell 'lego-shell-mode) - (setq proof-mode-for-pbp 'lego-pbp-mode)) + (setq proof-prog-name lego-prog-name + proof-mode-for-shell 'lego-shell-mode + proof-mode-for-response 'lego-response-mode + proof-mode-for-pbp 'lego-pbp-mode)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Configuring proof and pbp mode and setting up various utilities ;; @@ -365,7 +375,7 @@ (defun lego-init-syntax-table () "Set appropriate values for syntax table in current buffer." - (modify-syntax-entry ?_ "_") + (modify-syntax-entry ?_ "w") (modify-syntax-entry ?\' "_") (modify-syntax-entry ?\| ".") (modify-syntax-entry ?\* ". 23") @@ -525,7 +535,9 @@ We assume that module identifiers coincide with file names." (defun lego-pbp-mode-config () (setq pbp-change-goal "Next %s;" - pbp-error-regexp lego-error-regexp - )) + pbp-error-regexp lego-error-regexp) + (setq font-lock-keywords lego-font-lock-terms) + (proof-goals-config-done)) + (provide 'lego) |