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 | |
| parent | 4159c005b516ea482b6d0e5fc5e1d960348383c4 (diff) | |
implemented new buffer model. The goals buffer is now exclusively
reserved for goals.
Diffstat (limited to 'lego')
| -rw-r--r-- | lego/lego-syntax.el | 8 | ||||
| -rw-r--r-- | lego/lego.el | 26 |
2 files changed, 23 insertions, 11 deletions
diff --git a/lego/lego-syntax.el b/lego/lego-syntax.el index 20b0a326..f3a8f767 100644 --- a/lego/lego-syntax.el +++ b/lego/lego-syntax.el @@ -1,6 +1,6 @@ -;; lego-fontlock.el Font lock expressions for LEGO -;; Copyright (C) 1994, 1995, 1996, 1997 LFCS Edinburgh. -;; Author: Healfdene Goguen, Thomas Kleymann and Dilip Sequeira +;; lego-syntax.el Syntax of LEGO +;; Copyright (C) 1994 - 1998 LFCS Edinburgh. +;; Author: Thomas Kleymann and Dilip Sequeira ;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk> ;; Please let us know if you could maintain this package! ;; @@ -63,7 +63,7 @@ (list ; lambda binders - (list (lego-decl-defn-regexp "[:|]") 1 + (list (lego-decl-defn-regexp "[:|?]") 1 'proof-declaration-name-face) ; let binders 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) |