Cleaned ext.el up a bit in terms of its namespace and the management of

the comint filter.

2 files changed, 64 insertions, 79 deletions

diff --git a/ext.el b/ext.el
index ca2f9abc..ad38f248 100644
--- a/ext.el
+++ b/ext.el
@@ -12,7 +12,9 @@
 ; The annotation is then removed and stored in the extent's properties
 ; and the last bits are cleared.
 
-(defun analyse-structure ()
+(defvar *script-buffer*)
+
+(defun lego-pbp-analyse-structure ()
   (map-extents
       (lambda (ext maparg)
           (when (extent-property ext 'lego-pbp) (delete-extent ext))))
@@ -27,25 +29,25 @@
     (cond ((string= (char-to-string (preceding-char)) "%")
 	   (progn (delete-backward-char 1)(location-push (point))))
           ((string= (char-to-string (preceding-char)) "&")
-           (let ((previous-ampersand (location-pop)))
-             (if previous-ampersand (make-top-extent previous-ampersand))
+           (let ((prev-ampersand (location-pop)))
+             (if prev-ampersand (lego-pbp-make-top-extent prev-ampersand))
 	     (delete-backward-char 1)
 	     (location-push (point))))
-	  (t (make-pbp-extent))))
+	  (t (lego-pbp-make-extent))))
   (end-of-buffer)
-  (make-top-extent (location-pop)))
+  (lego-pbp-make-top-extent (location-pop)))
 
 
-(defun make-top-extent (previous-ampersand)
+(defun lego-pbp-make-top-extent (previous-ampersand)
   (save-excursion
     (beginning-of-line) (backward-char) 
     (let ((extent (make-extent previous-ampersand (point))))
       (set-extent-property extent 'mouse-face 'highlight)
       (set-extent-property extent 'lego-top-element 
-			   (compute-extent-name extent))
+			   (lego-pbp-compute-extent-name extent))
       (set-extent-property extent 'keymap *lego-pbp-keymap*))))
 
-(defun make-pbp-extent ()
+(defun lego-pbp-make-extent ()
    (let ((extent (make-extent (or (location-pop) 1) (point))))
 	 (set-extent-property extent 'mouse-face 'highlight)
 	 (set-extent-property extent 'keymap *lego-pbp-keymap*)
@@ -61,7 +63,7 @@
                         (goto-char (extent-end-position extent))
                         (delete-backward-char 1))))
 
-(defun compute-extent-name (extent)
+(defun lego-pbp-compute-extent-name (extent)
   (save-excursion
     (goto-char (extent-start-position extent))
     ; the search for an hypothesis name is ambiguous: any binder in
@@ -82,67 +84,53 @@
 ; last string that was processed was in the middle of a goal listing,
 ; in this case one must go on reading the rest of the goals.
 
-(defun lego-filter (string)
-     (cond ( *lego-in-goals-output*
-	  (save-excursion 
-	    (set-buffer *lego-goals* )
-	    (end-of-buffer)
-	    (insert-string string *lego-goals*)
-	    (lego-analyse-buffer)))
-         (t (save-excursion 
-	      (set-buffer *lego-tmp-goals*)
-	      (erase-buffer)
-	      (insert-string string)
-	      (end-of-buffer)
-	      (cond ((search-backward "-- Start of Goals --" () t)
-
-		     (end-of-line)
-		     (delete-region 1 (point))
-		     (set-buffer *lego-goals*)
-		     (erase-buffer)
-		     (insert-buffer *lego-tmp-goals*)
-		     (lego-analyse-buffer))
-		    ((search-backward "KillRef: ok, not in proof state" () t)
-		     (set-buffer *lego-goals*)
-		     (erase-buffer))
-		    ((search-backward "-- Pbp result --" () t)
-		     (end-of-line)
-		     (delete-region 1 (point))
-		     (search-forward "-- End Pbp result --" () t)
-		     (beginning-of-line)
-		     (delete-region (- (point) 1) (point-max))
-		     (if *script-buffer*
-			 (progn (set-buffer *script-buffer*)
-				(end-of-buffer)
-				(insert-buffer *lego-tmp-goals*)
-				(set-buffer *lego-tmp-goals*)))
-		     (proof-simple-send
-                          (buffer-substring 1 (point-max)))
-		     (erase-buffer)))))))
-
-
-(defun lego-analyse-buffer ()
-  (beginning-of-buffer)
-  (cond ((search-forward "*** QED ***" () t)
-	 (beginning-of-line)
-	 (delete-region 1 (point))
-	 (end-of-line)
-	 (delete-region (point) (point-max)))
-	((search-forward "-- End of Goals --" () t)
-	 (backward-char 18)
-	 (delete-region (point)(point-max))
-	 (setq *lego-in-goals-output* ())
-	 (analyse-structure))
-        (t (end-of-buffer)
-	   (setq *lego-in-goals-output* t))))
-
-(defvar *lego-in-goals-output* ())
+(defun lego-pbp-filter (string)
+  (save-excursion
+    (set-buffer *lego-tmp-goals*)
+    (goto-char (point-max))
+    (insert string)
+    (while (progn (goto-char (point-min))
+		  (re-search-forward proof-shell-prompt-pattern () t))
+      (narrow-to-region (point-min) (point))
+      (lego-pbp-process-region)
+      (delete-region (point-min) (point-max))
+      (widen))))
+
+(defun lego-pbp-process-region ()
+  (save-excursion 
+    (goto-char (point-min))
+    (cond ((search-forward "KillRef: ok, not in proof state" () t)
+	   (erase-buffer *lego-goals*))
+	  ((search-forward "*** QED ***" () t)
+	   (erase-buffer *lego-goals*)
+	   (insert-string "\n   *** QED ***" *lego-goals*))
+	  ((search-forward "-- Start of Goals --" () t)
+	   (delete-region (point-min) (point))
+	   (search-forward "-- End of Goals --" () t)
+	   (backward-char 18)
+	   (delete-region (point)(point-max))
+	   (set-buffer *lego-goals*)
+	   (erase-buffer)
+	   (insert-buffer-substring *lego-tmp-goals*)
+	   (lego-pbp-analyse-structure))
+	  ((search-forward "-- Pbp result --" () t)
+	   (end-of-line)
+	   (delete-region 1 (point))
+	   (search-forward "-- End Pbp result --" () t)
+	   (beginning-of-line)
+	   (delete-region (- (point) 1) (point-max))
+	   (proof-simple-send (buffer-substring 1 (point-max)))
+	   (if *script-buffer*
+	       (progn (set-buffer *script-buffer*)
+		      (end-of-buffer)
+		      (insert-buffer-substring *lego-tmp-goals*)))))))
 
-(defvar *script-buffer*)
 
 (defun lego-goals-init ()
   (setq *lego-tmp-goals* (get-buffer-create "*lego-tmp-goals*"))
   (setq *lego-goals* (get-buffer-create "*lego goals*"))
+  (erase-buffer *lego-goals*)
+  (erase-buffer *lego-tmp-goals*)
   (bury-buffer *lego-tmp-goals*))
 
 ; Now, using the extents in a mouse behavior is quite simple:
diff --git a/lego.el b/lego.el
index 6b7c41da..4126d5ea 100644
--- a/lego.el
+++ b/lego.el
@@ -4,7 +4,7 @@
 ;; code.
 
 ;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk>
-;; Time-stamp: <13 Nov 96 tms /home/tms/elisp/lego.el>
+;; Time-stamp: <05 Nov 96 tms /home/tms/elisp/lego.el>
 ;; Thanks to David Aspinall, Robert Boyer, Rod Burstall,
 ;;           James McKinna, Mark Ruys, Martin Steffen, Perdita Stevens  
 
@@ -25,7 +25,7 @@
   is primarily concerned to make life easier. There it will enable
   pretty printing")
 
-(defconst lego-pretty-on "Configure PrettyOn; Configure AnnotateOn;"
+(defconst lego-pretty-on "Configure PrettyOn;"
   "Command to enable pretty printing of the LEGO process.")
 
 (defconst lego-pretty-set-width "Configure PrettyWidth %s;"
@@ -96,7 +96,7 @@
 (defvar lego-shell-process-name "lego"
   "*The name of the lego-process")
 
-(defvar lego-shell-prog-name "lego"
+(defvar lego-shell-prog-name "~djs/lego/lego/bin/legoML"
   "*Name of program to run as lego.")
 
 (defvar lego-shell-working-dir ""
@@ -109,11 +109,10 @@
 
 (defvar lego-goal-regexp "?[0-9]+  : ")
 
-(defvar lego-outline-regexp
-  (concat "[[*]\\|"
-	  (ids-to-regexp 
-	   '("Discharge" "DischargeKeep" "Freeze" "$?Goal" "Module" "Record" "Inductive"
-     "Unfreeze"))))
+(defvar lego-outline-regexp 
+  (ids-to-regexp 
+   '("*" "Discharge" "Freeze" "Goal" "Module" "[" "Record" "Inductive" 
+     "Unfreeze")))
 
 (defvar lego-outline-heading-end-regexp ";\\|\\*)")
 
@@ -123,10 +122,10 @@
 ;; ----- keywords for font-lock. If you want to hack deeper, you'd better
 ;; ----- be fluent in regexps - it's in the YUK section.
 
-(defvar lego-keywords-goal '("$?Goal"))
+(defvar lego-keywords-goal '("Goal"))
 
 (defvar lego-keywords-save
-  '("$?Save"))
+  '("Save" "SaveFrozen" "SaveUnfrozen"))
 
 (defvar lego-keywords
   (append lego-keywords-goal lego-keywords-save '("andI" "Claim"
@@ -302,9 +301,8 @@
 	   (list (concat "^  \\(" lego-id "\\) = ... :") 1 
 			 'font-lock-function-name-face)
 
-	   (list (concat "^  \\(" lego-id "\\( " lego-id "\\)*\\) [:|] ") 1 
+	   (list (concat "^  \\(" lego-id "\\) : ") 1 
 			 'font-lock-declaration-name-face)
-           ; e.g., decl S1 S2 : prog sort
 
 	   (list (concat "\\<decl\\>  \\(" lego-id "\\) [:|]") 1 
 			 'font-lock-declaration-name-face)
@@ -467,7 +465,7 @@
   (setq compilation-search-path (cons nil (lego-get-path)))
   (add-hook 'proof-safe-send-hook 'lego-adjust-line-width)
   (add-hook 'proof-shell-exit-hook 'lego-shell-zap-line-width)
-  (add-hook 'comint-output-filter-functions 'lego-filter t)
+  (add-hook 'comint-output-filter-functions 'lego-pbp-filter t)
   (lego-goals-init)
   (font-lock-fontify-buffer))
 
@@ -523,7 +521,6 @@
   (modify-syntax-entry ?\* ". 23")
   (modify-syntax-entry ?\( "()1")
   (modify-syntax-entry ?\) ")(4")
-  (setq blink-matching-paren-dont-ignore-comments t)
 
   (proof-config-done)