From 61f33b67ba63df3542e493a40a2d348323f2558b Mon Sep 17 00:00:00 2001
From: Thomas Kleymann
Date: Tue, 15 Sep 1998 13:32:27 +0000
Subject: Reimplemented proof-shell-popup-eager-annotation

These are no longer displayed in the *GOALS* buffer.
---
 lego/lego-syntax.el |  5 ++---
 lego/lego.el        | 10 +++++++---
 2 files changed, 9 insertions(+), 6 deletions(-)

(limited to 'lego')

diff --git a/lego/lego-syntax.el b/lego/lego-syntax.el
index f9fb52d2..9d770a43 100644
--- a/lego/lego-syntax.el
+++ b/lego/lego-syntax.el
@@ -34,9 +34,8 @@
 (defconst lego-tacticals '("Then" "Else" "Try" "Repeat" "For"))
 
 ;; ----- regular expressions for font-lock
-(defvar lego-error-regexp "^\\(Error\\|Lego parser\\)"
-  "A regular expression indicating that the LEGO process has
-  identified an error.") 
+(defconst lego-error-regexp "^\\(Error\\|Lego parser\\)"
+  "A regular expression indicating that the LEGO process has identified an error.") 
 
 (defvar lego-id proof-id)
 
diff --git a/lego/lego.el b/lego/lego.el
index 2b83e51a..aed76bdf 100644
--- a/lego/lego.el
+++ b/lego/lego.el
@@ -427,8 +427,6 @@
 		       ("lego"  . lego-tags))
 		     tag-table-alist)))
 
-  (setq font-lock-keywords lego-font-lock-keywords-1)
-
 ;; where to find files
 
   (setq compilation-search-path (cons nil (lego-get-path)))
@@ -437,6 +435,8 @@
 
 ;; font-lock
 
+  (setq font-lock-keywords lego-font-lock-keywords-1)
+
 ;; if we don't have the following in xemacs, zap-commas fails to work.
 
   (and (boundp 'font-lock-always-fontify-immediately)
@@ -475,7 +475,11 @@
         proof-shell-init-cmd lego-process-config
 	proof-analyse-using-stack nil
 	proof-shell-process-output-system-specific lego-shell-process-output
-        lego-shell-current-line-width nil)
+        lego-shell-current-line-width nil
+
+	;;FIXME: we ought to set up separate font-lock instructions for
+	;;the shell, the goal buffer and the script
+	font-lock-keywords lego-font-lock-keywords-1)
 
   (lego-init-syntax-table)
 
-- 
cgit v1.2.3