added font-lock properties for pbp-lego-mode

1 files changed, 41 insertions, 25 deletions

diff --git a/lego.el b/lego.el
index e049ee2c..27e888ba 100644
--- a/lego.el
+++ b/lego.el
@@ -4,7 +4,7 @@
 ;; code.
 
 ;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk>
-;; Time-stamp: <03 Dec 96 tms /home/tms/elisp/lego.el>
+;; Time-stamp: <05 Dec 96 tms /home/tms/elisp/lego.el>
 ;; Thanks to David Aspinall, Robert Boyer, Rod Burstall,
 ;;           James McKinna, Mark Ruys, Martin Steffen, Perdita Stevens  
 
@@ -173,6 +173,9 @@
    "lego" "Lego Mode"
    (lego-mode-config))
 
+(define-derived-mode lego-pbp-mode pbp-mode
+  "pbp" "Proof-by-pointing support for LEGO"
+  (lego-pbp-mode-config))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;; Popup and Pulldown Menu ;;;
@@ -275,20 +278,37 @@
 ;              [        sort        [n:nat]                  =
 ;              [        sort        [abbrev=...][n:nat]      =
 
-(defvar lego-font-lock-keywords-1
-   (list
-
-     (cons (ids-to-regexp lego-keywords) 'font-lock-keyword-face)
-     (cons (ids-to-regexp lego-tacticals) 'font-lock-tacticals-name-face)
+(defvar lego-font-lock-terms
+  (list
 
+   ; lambda binders
      (list (lego-decl-defn-regexp "[:|]") 1
 	   'font-lock-declaration-name-face)
+
+     ; let binders
      (list (lego-decl-defn-regexp "=") 1 'font-lock-function-name-face)
 
+     ; Pi and Sigma binders
      (list (concat "[{<]\\s *\\(" lego-ids "\\)") 1
-;            ^  Pi binder
-;             ^ Sigma binder            
-		   'font-lock-declaration-name-face)
+	   'font-lock-declaration-name-face)
+   
+     ;; Kinds
+     (cons (concat "\\<Prop\\>\\|\\<Type\\s *\\(("
+		   lego-id ")\\)?") 'font-lock-type-face))
+  "*Font-lock table for LEGO terms.")
+
+(defvar lego-font-lock-error-messages
+  (list '("attempt to apply\\|with domain type\\|^to " .font-lock-error-face)
+	  (cons (concat lego-error-regexp ".*\n")
+		      'font-lock-error-face))
+  "Font-lock table for Error messages generated by the LEGO process.")
+
+(defvar lego-font-lock-keywords-1
+   (append
+    lego-font-lock-terms
+    (list
+     (cons (ids-to-regexp lego-keywords) 'font-lock-keyword-face)
+     (cons (ids-to-regexp lego-tacticals) 'font-lock-tacticals-name-face)
 
      (list (concat "\\("
 		   (ids-to-regexp lego-keywords-goal)
@@ -298,11 +318,8 @@
      (list (concat "\\("
 		   (ids-to-regexp lego-keywords-save)
 		   "\\)\\s *\\(" lego-id "\\)")
-             2 'font-lock-function-name-face)
-
-     ;; Kinds
-     (cons (concat "\\<Prop\\>\\|\\<Type\\s *\\(("
-		   lego-id ")\\)?") 'font-lock-type-face)))
+             2 'font-lock-function-name-face))))
+     
 
 (defvar lego-shell-font-lock-keywords-1
   (append lego-font-lock-keywords-1
@@ -328,14 +345,7 @@
 			 'font-lock-declaration-name-face)
 		 
 	   (list (concat "^value = \\(" lego-id "\\)") 1
-			 'font-lock-declaration-name-face)
-
-	  ;; Error Messages (only required in the process buffer)
-
-	  '("attempt to apply\\|with domain type\\|^to " .font-lock-error-face)
-	  (cons (concat lego-error-regexp ".*\n")
-		      'font-lock-error-face))))
-
+			 'font-lock-declaration-name-face))))
 ;;
 ;; A big hack to unfontify commas in declarations and definitions. All
 ;; that can be said for it is that the previous way of doing this was
@@ -480,6 +490,7 @@
   (setq proof-shell-buffer-name (concat "*" lego-shell-process-name "*"))
   (setq proof-shell-prompt-pattern lego-shell-prompt-pattern)
   (setq proof-shell-mode-is 'lego-shell-mode)
+  (setq pbp-mode-is 'lego-pbp-mode)
   (setq proof-shell-abort-goal-regexp lego-shell-abort-goal-regexp)
   (setq proof-shell-proof-completed-regexp lego-shell-proof-completed-regexp)
   (setq proof-shell-change-goal "Next %s;")
@@ -531,9 +542,9 @@
     (proof-simple-send 
      (concat lego-make-command " \"" file "\";") t)))
 
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;   Configuring proof mode and setting up various utilities        ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;   Configuring proof and pbp mode and setting up various utilities  ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 (defun lego-common-config ()
 
@@ -642,4 +653,9 @@
   (setq font-lock-keywords lego-shell-font-lock-keywords-1)
 )
 
+(defun lego-pbp-mode-config ()
+  (lego-common-config)
+  (setq font-lock-keywords
+	(append lego-font-lock-terms lego-font-lock-error-messages)))
+
 (provide 'lego)