diff options
| author |  Thomas Kleymann <da+pg-tms@inf.ed.ac.uk> | 1998-09-15 13:32:27 +0000 |
|---|---|---|
| committer | Thomas Kleymann <da+pg-tms@inf.ed.ac.uk> | 1998-09-15 13:32:27 +0000 |
| commit | 61f33b67ba63df3542e493a40a2d348323f2558b (patch) | |
| tree | 1cfeae63b1a7bc002474fddd1665a04e30d85246 /lego | |
| parent | 3d4cacefd464d805dab26bda845bf7a5e1a5de9e (diff) | |
Reimplemented proof-shell-popup-eager-annotation
These are no longer displayed in the *GOALS* buffer.
Diffstat (limited to 'lego')
| -rw-r--r-- | lego/lego-syntax.el | 5 | ||||
| -rw-r--r-- | lego/lego.el | 10 |
2 files changed, 9 insertions, 6 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) 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) |