aboutsummaryrefslogtreecommitdiffhomepage
path: root/lego/lego-syntax.el
diff options
context:
space:
mode:
authorGravatar Thomas Kleymann <da+pg-tms@inf.ed.ac.uk>1998-09-15 13:32:27 +0000
committerGravatar Thomas Kleymann <da+pg-tms@inf.ed.ac.uk>1998-09-15 13:32:27 +0000
commit61f33b67ba63df3542e493a40a2d348323f2558b (patch)
tree1cfeae63b1a7bc002474fddd1665a04e30d85246 /lego/lego-syntax.el
parent3d4cacefd464d805dab26bda845bf7a5e1a5de9e (diff)
Reimplemented proof-shell-popup-eager-annotation
These are no longer displayed in the *GOALS* buffer.
Diffstat (limited to 'lego/lego-syntax.el')
-rw-r--r--lego/lego-syntax.el5
1 files changed, 2 insertions, 3 deletions
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)