merged script management (1.10.2.18) with main branch

1 files changed, 88 insertions, 94 deletions

diff --git a/proof.el b/proof.el
index b1c88d42..92db0b94 100644
--- a/proof.el
+++ b/proof.el
@@ -7,26 +7,31 @@
 ;;           James McKinna, Mark Ruys, Martin Steffen, Perdita Stevens  
 
 
+
 ;; TO DO:
 
 ;; o Need to think about fixing up errors caused by pbp-generated commands
 
-;; o Proof mode breaks if an error is encountered during the import
-;;   phase. 
-
-;; o proof-undo-last-successful-command needs to be extended so that
-;;   it deletes regions of the script buffer when invoked outside a proof 
-
 ;; o undo support needs to consider Discharge; perhaps unrol to the
 ;;   beginning of the module? 
 
+;; o pbp code is horribly inefficient and doesn't accord with the tech
+;;   report
+
 ;; $Log$
-;; Revision 1.12  1997/10/14 09:29:17  tms
-;; proof-process-active-terminator is now an extension of
-;; proof-assert-until-point (it was broken and looks healthier now)
+;; Revision 1.13  1997/10/16 08:48:56  tms
+;; merged script management (1.10.2.18) with main branch
+;;
+;; Revision 1.10.2.18  1997/10/14 19:30:55  djs
+;; Bug fixes for comments.
 ;;
-;; Revision 1.11  1997/10/13 17:09:52  tms
-;; put script-management branch back on main branch
+;; Revision 1.10.2.17  1997/10/14 17:30:15  djs
+;; Fixed a bunch of bugs to do with comments, moved annotations out-of-band
+;; to exploit a feature which will exist in XEmacs 20. (One day there *will
+;; be* lemon-scented paper napkins). Added code to detect failing imports.
+;;
+;; Revision 1.10.2.16  1997/10/10 19:24:33  djs
+;; Attempt to create a fresh branch because of Attic-Attack.
 ;;
 ;; Revision 1.10.2.15  1997/10/10 19:20:01  djs
 ;; Added multiple file support, changed the way comments work, fixed a
@@ -95,8 +100,7 @@
 (defvar proof-goal-command-regexp nil "Matches a goal command")
 (defvar proof-goal-with-hole-regexp nil "Matches a saved goal command")
 
-(defvar proof-undo-target-fn nil "Compute how to undo to this extent")
-(defvar proof-forget-target-fn nil "Compute how to forget back to this ext")
+(defvar proof-retract-target-fn  nil "Compute how to retract a target segment")
 (defvar proof-kill-goal-command nil "How to kill a goal.")
 
 (defvar pbp-change-goal nil
@@ -154,7 +158,7 @@
 (defvar proof-shell-end-goals-regexp ""
   "String indicating the end of the proof state.")
 
-(defvar proof-shell-sanitise t "sanitise output?")
+(defvar proof-shell-sanitise nil "sanitise output?")
 
 (defvar pbp-error-regexp nil
   "A regular expression indicating that the PROOF process has
@@ -257,46 +261,46 @@
 ;;  Note that we need to go back to using marks too                 ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
-(defun make-span (start end)
+(defsubst make-span (start end)
   (make-extent start end))
 
-(defun set-span-endpoints (span start end)
+(defsubst set-span-endpoints (span start end)
   (set-extent-endpoints span start end))
 
-(defun set-span-start (span value)
+(defsubst set-span-start (span value)
   (set-extent-endpoints span value (extent-end-position span)))
 
-(defun set-span-end (span value)
+(defsubst set-span-end (span value)
   (set-extent-endpoints span (extent-start-position span) value))
 
-(defun span-property (span name)
+(defsubst span-property (span name)
   (extent-property span name))
 
-(defun set-span-property (span name value)
+(defsubst set-span-property (span name value)
   (set-extent-property span name value))
 
-(defun delete-span (span)
+(defsubst delete-span (span)
   (delete-extent span))
 
-(defun delete-spans (start end prop)
+(defsubst delete-spans (start end prop)
   (mapcar-extents 'delete-extent nil (current-buffer) start end  nil prop))
 
-(defun span-at (pt prop)
+(defsubst span-at (pt prop)
   (extent-at pt nil prop))
 
-(defun span-at-before (pt prop)
+(defsubst span-at-before (pt prop)
   (extent-at pt nil prop nil 'before))
   
-(defun span-start (span)
+(defsubst span-start (span)
   (extent-start-position span))
 
-(defun span-end (span)
+(defsubst span-end (span)
   (extent-end-position span))
 
-(defun prev-span (span prop)
+(defsubst prev-span (span prop)
   (extent-at (extent-start-position span) nil prop nil 'before))
 
-(defun next-span (span prop)
+(defsubst next-span (span prop)
   (extent-at (extent-end-position span) nil prop nil 'after))
 
 (defvar proof-locked-ext nil
@@ -574,10 +578,10 @@
 	   ((= c proof-shell-goal-char)
 	    (setq topl (append topl (list (+ 1 op)))))
 	   ((= c proof-shell-start-char)	    
-	    (setq ap (- (aref string (incf ip)) 32))
+	    (setq ap (- (aref string (incf ip)) 128))
 	    (incf ip)
 	    (while (not (= (aref string ip) proof-shell-end-char))
-	      (aset ann ap (- (aref string ip) 32))
+	      (aset ann ap (- (aref string ip) 128))
 	      (incf ap)
 	      (incf ip))
 	    (setq stack (cons op (cons (substring ann 0 ap) stack))))
@@ -648,7 +652,8 @@
 (defun proof-shell-process-output (cmd string)
   (cond 
    ((string-match proof-shell-error-regexp string)
-    (cons 'error (proof-shell-strip-annotations string)))
+    (cons 'error (proof-shell-strip-annotations 
+		  (substring string (match-beginning 0)))))
 
    ((string-match proof-shell-abort-goal-regexp string)
     (setq proof-shell-delayed-output (cons 'insert "\n\nAborted"))
@@ -663,7 +668,7 @@
       (while (progn (setq start (match-end 0))
 		    (string-match proof-shell-start-goals-regexp 
 				  string start)))
-      (string-match proof-shell-end-goals-regexp string start)
+      (setq end (string-match proof-shell-end-goals-regexp string start))
       (setq proof-shell-delayed-output 
 	    (cons 'analyse (substring string start end)))))
        
@@ -835,6 +840,19 @@ at the end of locked region (after inserting a newline)."
 	       (t (if (proof-shell-exec-loop)
 		      (proof-shell-handle-delayed-output)))))))))
 
+(defun proof-last-goal-or-goalsave ()
+  (save-excursion
+    (let ((ext (span-at-before (proof-end-of-locked) 'type)))
+    (while (and ext 
+		(not (eq (span-property ext 'type) 'goalsave))
+		(or (eq (span-property ext 'type) 'comment)
+		    (not (string-match proof-goal-command-regexp 
+				       (span-property ext 'cmd)))))
+      (setq ext (prev-span ext 'type)))
+    ext)))
+    
+
+
 (defun proof-steal-process ()
   (proof-start-shell)
   (if proof-shell-busy (error "Proof Process Busy!"))
@@ -858,14 +876,9 @@ at the end of locked region (after inserting a newline)."
 	(if (not (y-or-n-p "Reprocess this file? " )) (error "Aborted")))
       (save-excursion
 	(set-buffer proof-script-buffer)
-	(setq ext (span-at-before (proof-end-of-locked) 'type))
-	(while (and ext (not (memq (span-property ext 'type)
-				   '(goalsave comment)))
-		    (not (string-match "^Goal" (span-property ext 'cmd))))
-	  (setq ext (prev-span ext 'type)))
-	(setq cmd (if (and ext (let ((cmd  (span-property ext 'cmd)))
-				 (and cmd (string-match "^Goal" cmd))))
-		      "KillRef; " ""))
+	(setq ext (proof-last-goal-or-goalsave))
+	(setq cmd (if (and ext (not (eq (span-property ext 'type) 'goalsave)))
+		      proof-kill-goal-command ""))
 	(proof-segment-buffer nil nil)
 	(delete-spans (point-min) (point-max) 'type))      
       (setq proof-script-buffer (current-buffer))
@@ -943,9 +956,9 @@ at the end of locked region (after inserting a newline)."
 	(delete-span gext)
 	(setq gext next))
       (if (null nam)
-	    (if (let ((cmd (span-property gext 'cmd)))
-		  (and cmd (string-match proof-goal-with-hole-regexp cmd)))
-		(setq nam (match-string 1 cmd))
+	    (if (string-match proof-goal-with-hole-regexp
+			      (span-property gext 'cmd))
+		(setq nam (match-string 2 cmd))
 	      (error "Oops... can't find Goal name!!!")))
 	(set-span-end gext end)
 	(set-span-property gext 'highlight 'mouse-face)
@@ -1030,17 +1043,18 @@ at the end of locked region (after inserting a newline)."
 the documentation for `proof-retract-until-point'. It optionally
 deletes the region corresponding to the proof sequence."
   (let ((start (span-start ext))
-        (end (span-end ext)))
+        (end (span-end ext))
+	(kill (span-property ext 'delete-me)))
     (proof-segment-buffer start proof-queue-loose-end)
     (delete-spans start end 'type)
     (delete-span ext)
-    (if delete-region (delete-region start end))))
+    (if kill delete-region start end)))
 
+(defun proof-setup-retract-action (start end proof-command delete-region)
+  (let ((span (make-span start end)))
+    (set-span-property span 'delete-me delete-region)
+    (list (list span proof-command 'proof-done-retracting))))
 
-(defun proof-retract-setup-actions (start end proof-command delete-region)
-  (list (list (make-span start end)
-	      proof-command
-	      `(lambda (ext) (proof-done-retracting ext ,delete-region)))))
 
 (defun proof-retract-until-point (&optional delete-region)
   "Sets up the proof process for retracting until point. In
@@ -1050,47 +1064,11 @@ deletes the region corresponding to the proof sequence."
    the proof script corresponding to the proof command sequence."
   (interactive)
   (proof-check-process-available)
-  (let ((sext (span-at (point) 'type))
-	(end (proof-end-of-locked))
-	ext start actions)
-    (if (null end) (error "No locked region"))
-    (if (or (null sext) (< end (point))) (error "Outside locked region"))
-
-    (setq start (span-start sext))
-    (setq ext (span-at-before end 'type))
-    (while (let ((cmd (span-property ext 'cmd)))
-	     (and ext cmd
-		  (not (string-match proof-goal-command-regexp cmd))
-		  (not (eq (span-property ext 'type) 'goalsave))))
-      (setq ext (prev-span ext 'type)))
+  (let ((sext (span-at (point) 'type)))
+    (if (null (proof-end-of-locked)) (error "No locked region"))
+    (if (null sext) (error "Outside locked region"))
+    (funcall proof-retract-target-fn sext delete-region)))
 
-    (if (let ((cmd (span-property ext 'cmd)))
-	  (and ext cmd (string-match proof-goal-command-regexp cmd)))
-	(if (<= (span-end ext) (point))
-	    (progn
-	      (setq ext sext)
-	      (while (and ext (eq (span-property ext 'type) 'comment))
-		(setq ext (next-span ext 'type)))
-	      (setq actions (proof-retract-setup-actions
-			     start end 
-			     (if (null ext) "COMMENT" 
-			       (funcall proof-undo-target-fn ext))
-			     delete-region)
-		    end start))
-	  
-	  (setq actions	(proof-retract-setup-actions (span-start ext) end
-						     proof-kill-goal-command
-						     delete-region)
-		end (span-start ext))))
-
-    (if (> end start) 
-	(setq actions 
-	      (nconc (proof-retract-setup-actions 
-		      start end
-		      (funcall proof-forget-target-fn sext)
-		      delete-region)
-		     actions)))
-    (proof-start-queue (min start end) (proof-end-of-locked) actions)))
 
 (defun proof-undo-last-successful-command ()
   "Undo last successful command, both in the buffer recording the
@@ -1103,14 +1081,16 @@ deletes the region corresponding to the proof sequence."
 (defun proof-restart-script ()
   (interactive)
   (save-excursion
-    (set-buffer proof-script-buffer)
-    (delete-spans (point-min) (point-max) 'type)
-    (proof-segment-buffer nil nil)
+    (if (buffer-live-p proof-script-buffer)
+	(progn
+	  (set-buffer proof-script-buffer)
+	  (delete-spans (point-min) (point-max) 'type)
+	  (proof-segment-buffer nil nil)))
     (setq proof-shell-busy nil
 	  proof-script-buffer nil)
-    (if (get-buffer proof-shell-buffer) 
+    (if (buffer-live-p proof-shell-buffer) 
 	(kill-buffer proof-shell-buffer))
-    (if (get-buffer proof-pbp-buffer)
+    (if (buffer-live-p proof-pbp-buffer)
 	(kill-buffer proof-pbp-buffer))))
 
 	  
@@ -1230,6 +1210,20 @@ current command."
   (add-hook 'comint-output-filter-functions 'proof-shell-filter nil t)
 ;  (add-hook 'comint-output-filter-functions 'comint-truncate-buffer nil t)
 ;  (setq comint-buffer-maximum-size 10000)
+;
+
+;; Can't get this to work in XEmacs 19.15, probably because specifiers
+;; are not fully implemented. So instead:
+
+  (setq proof-shell-sanitise t)
+
+;  (let ((disp (make-display-table))
+;	(i 128))
+;	(while (< i 256)
+;	  (aset disp i "")
+;	  (incf i))
+;	(set-specifier current-display-table disp))
+		  
   (setq comint-append-old-input nil)
   (setq proof-mark-ext (make-extent nil nil (current-buffer)))
   (set-span-property proof-mark-ext 'detachable nil)