FIRST ATTEMPT AT CANY QUEUE HANDLING. Extending regions when advancing patch.

3 files changed, 120 insertions, 55 deletions

diff --git a/generic/proof-script.el b/generic/proof-script.el
index 7ab92c94..c5404139 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -595,7 +595,7 @@ a scripting buffer is killed it is always retracted."
 	      ;; And now there is no active scripting buffer
 	      (setq proof-script-buffer nil))))))
   
-(defun proof-activate-scripting (&optional nosaves)
+(defun proof-activate-scripting (&optional nosaves queuemode)
   "Ready prover and activate scripting for the current script buffer.
 
 The current buffer is prepared for scripting. No changes are
@@ -609,10 +609,15 @@ user wants to save some buffers; this is done if the user
 option `proof-query-file-save-when-activating-scripting' is set
 and provided the optional argument NOSAVES is non-nil.
 
+The optional argument QUEUEMODE relaxes the test for a
+busy proof shell to allow one which has mode QUEUEMODE.
+In all other cases, a proof shell busy error is given.
+
 Finally, the hooks `proof-activate-scripting-hook' are run.  
 This can be a useful place to configure the proof assistant for
 scripting in a particular file, for example, loading the
 correct theory, or whatever."
+  (interactive)
   ;; FIXME: the scope of this save-excursion is rather wide.
   ;; Problems without it however: Use button behaves oddly
   ;; when process is started already.
@@ -620,7 +625,7 @@ correct theory, or whatever."
   ;; First experiment shows that it's the hooks that cause
   ;; problem, maybe even the use of proof-cd-sync (can't see why).
   (save-excursion
-    (proof-shell-ready-prover)
+    (proof-shell-ready-prover queuemode)
     (cond 
      ((not (eq proof-buffer-type 'script)) 
       (error "Must be running in a script buffer!"))
@@ -954,7 +959,7 @@ the ACS is marked in the current buffer. If CMD does not match any,
 ;; may be helpful here.
 
 (defun proof-segment-up-to (pos &optional next-command-end)
-  "Create a list of (type,int,string) tuples from end of locked region to POS.
+  "Create a list of (type,int,string) tuples from end of queue/locked region to POS.
 Each tuple denotes the command and the position of its terminator,
 type is one of 'comment, or 'cmd. 'unclosed-comment may be consed onto
 the start if the segment finishes with an unclosed comment.
@@ -965,9 +970,9 @@ the next command end."
       ;; quote-parity is false if we're inside quotes.
       ;; Only one of (depth > 0) and (not quote-parity)
       ;; should be true at once. -- hhg
-    (let ((str (make-string (- (buffer-size)
-			       (proof-unprocessed-begin) -10) ?x))
-	  (i 0) (depth 0) (quote-parity t) done alist c
+    (let* ((start	(proof-queue-or-locked-end))
+	   (str		(make-string (- (buffer-size) start -10) ?x))
+	   (i 0) (depth 0) (quote-parity t) done alist c
 	  (comment-end-regexp (regexp-quote proof-comment-end))
 	  (comment-start-regexp (regexp-quote proof-comment-start)))
 	  ;; For forthcoming improvements: skip over boring
@@ -978,7 +983,6 @@ the next command end."
 	  ;	   (substring proof-comment-end 1 1)
 	  ;	   (char-to-string proof-terminal-char)
 	  ;	   "\"")))
-     (proof-goto-end-of-locked)
      (while (not done)
        (cond
 	;; Case 1. We've reached POS, not allowed to go past it,
@@ -1149,7 +1153,7 @@ UNCLOSED-COMMENT-FUN. If IGNORE-PROOF-PROCESS-P is set, no commands
 will be added to the queue and the buffer will not be activated for
 scripting."
   (unless ignore-proof-process-p 
-    (proof-activate-scripting))
+    (proof-activate-scripting nil 'advancing))
   (let ((semis))
     (save-excursion
       ;; Give error if no non-whitespace between point and end of locked region.
@@ -1164,11 +1168,11 @@ scripting."
 	(funcall unclosed-comment-fun)
       (if (eq 'unclosed-comment (car semis)) (setq semis (cdr semis)))
       (if (and (not ignore-proof-process-p) (null semis))
-	  (error "I can't see any complete commands to process!"))
+	  (error "I can't find any complete commands to process!"))
       (goto-char (nth 2 (car semis)))
       (and (not ignore-proof-process-p)
 	   (let ((vanillas (proof-semis-to-vanillas (nreverse semis))))
-	     (proof-start-queue (proof-unprocessed-begin) (point) vanillas))))))
+	     (proof-extend-queue (point) vanillas))))))
 
 
 ;; da: This is my alternative version of the above.
@@ -1203,7 +1207,7 @@ Afterwards, move forward to near the next command afterwards, unless
 DONT-MOVE-FORWARD is non-nil.  If FOR-NEW-COMMAND is non-nil,
 a space or newline will be inserted automatically."
   (unless ignore-proof-process-p
-    (proof-activate-scripting))
+    (proof-activate-scripting nil 'advancing))
   (or ignore-proof-process-p
       (if (proof-locked-region-full-p)
 	  (error "Locked region is full, no more commands to do!")))
@@ -1229,7 +1233,7 @@ a space or newline will be inserted automatically."
       (if (not ignore-proof-process-p)
 	   (let ((vanillas (proof-semis-to-vanillas (nreverse semis))))
 ;	     (if crowbar (setq vanillas (cons crowbar vanillas)))
-	     (proof-start-queue (proof-unprocessed-begin) (point) vanillas)))
+	     (proof-extend-queue (point) vanillas)))
       ;; This is done after the queuing to be polite: it means the
       ;; spacing policy enforced here is not put into the locked
       ;; region so the user can re-edit.
@@ -1308,32 +1312,60 @@ Optionally delete the region corresponding to the proof sequence."
   "Retract the span TARGET and delete it if DELETE-REGION is non-nil.
 Notice that this necessitates retracting any spans following TARGET,
 up to the end of the locked region."
-  (let ((end (proof-locked-end))
+  (let ((end   (proof-unprocessed-begin))
 	(start (span-start target))
-	(span (proof-last-goal-or-goalsave))
+	(span  (proof-last-goal-or-goalsave))
 	actions)
+
+    ;; Examine the last span in the locked region.  
     
+    ;; If the last goal or save span is not a goalsave (i.e. it's
+    ;; open) we examine to see how to remove it
     (if (and span (not (eq (span-property span 'type) 'goalsave)))
+	;; If the goal or goalsave span ends before the target span,
+	;; then we are retracting within the last unclosed proof,
+	;; and the retraction just amounts to a number of undo
+	;; steps.  
+	;; FIXME: really, there shouldn't be more work to do: so
+	;;  why call proof-find-and-forget-fn later?
 	(if (< (span-end span) (span-end target))
 	    (progn
+	      ;; Skip comment spans at and immediately following target
 	      (setq span target)
 	      (while (and span (eq (span-property span 'type) 'comment))
 		(setq span (next-span span 'type)))
+	      ;; Calculate undos for the current open segment
+	      ;; of proof commands
 	      (setq actions (proof-setup-retract-action
 			     start end 
 			     (if (null span) proof-no-command
 			       (funcall proof-count-undos-fn span))
 			     delete-region)
 		    end start))
-	  
+	  ;; Otherwise, start the retraction by killing off the
+	  ;; currently active goal.
+	  ;; FIXME: and couldn't we move the end upwards?
 	  (setq actions 
 		(proof-setup-retract-action (span-start span) end
 					    proof-kill-goal-command
 						    delete-region)
 		end (span-start span))))
-    
+    ;; Check the start of the target span lies before the end
+    ;; of the locked region (should always be true since we don't
+    ;; make spans outside the locked region at the moment)...
     (if (> end start) 
 	(setq actions
+	      ;; Append a retract action to clear the entire
+	      ;; start-end region.  Rely on proof-find-and-forget-fn
+	      ;; to calculate a command which "forgets" back to
+	      ;; the first definition, declaration, or whatever
+	      ;; that comes after the target span.
+	      ;; FIXME: originally this assumed a linear context, 
+	      ;; and that forgetting the first thing  forgets all 
+	      ;; subsequent ones.  it might be more general to 
+	      ;; allow *several* commands, and even queue these
+	      ;; separately for each of the spans following target
+	      ;; which are concerned.
 	      (nconc actions (proof-setup-retract-action 
 			      start end
 			      (funcall proof-find-and-forget-fn target)
@@ -1363,6 +1395,8 @@ If DELETE-REGION is non-nil, delete the region in the proof script
 corresponding to the proof command sequence.
 If invoked outside a locked region, undo the last successfully processed
 command."
+  ;; Make sure we're ready
+  ;; FIXME: next step in extend regions: (proof-activate-scripting nil 'retracting)
   (proof-activate-scripting)
   (let ((span (span-at (point) 'type)))
     ;; FIXME da: shouldn't this test be earlier??
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 34c6eff4..50f9a557 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -142,11 +142,15 @@ For LEGO 1.3.1 use `nil', for Coq 6.2, use `t'.")
 ;;
 ;;  -da.
 
-(defun proof-shell-ready-prover ()
+(defun proof-shell-ready-prover (&optional queuemode)
   "Make sure the proof assistant is ready for a command.
+If QUEUEMODE is set, succeed if the proof shell is busy but
+has mode QUEUEMODE.
+Otherwise, if the shell is busy, give an error.
 No change to current buffer or point."
   (proof-shell-start)
-  (if proof-shell-busy (error "Proof Process Busy!")))
+  (unless (or (not proof-shell-busy) (eq queuemode proof-shell-busy))
+    (error "Proof Process Busy!")))
 
 (defun proof-shell-live-buffer ()
   "Return buffer of active proof assistant, or nil if none running."
@@ -160,11 +164,12 @@ No error messages.  Useful as menu or toolbar enabler."
   (and (proof-shell-live-buffer)
        (not proof-shell-busy)))
 
-(defun proof-grab-lock ()
+(defun proof-grab-lock (&optional queuemode)
   "Grab the proof shell lock, starting the proof assistant if need be.
-Runs proof-state-change-hook to notify state change."
+Runs proof-state-change-hook to notify state change.
+If QUEUEMODE is supplied, set the lock to that value."
   (proof-shell-ready-prover)
-  (setq proof-shell-busy t)
+  (setq proof-shell-busy (or queuemode t))
   (run-hooks 'proof-state-change-hook))
 
 (defun proof-release-lock ()
@@ -228,10 +233,15 @@ Does nothing if proof assistant is already running."
 
     ;; da: We don't really need this.  We never have more than
     ;; one proof shell running at a time.  We might as well
-    ;; kill off the old buffer anyway.  But leave it in for now for
-    ;; future expansion, or for user to inspect the old buffer.
-
-    ;; da: Removed this because it leads to objectionable 
+    ;; kill off the old buffer anyway.  Only possible use is
+    ;; for future expansion, or for user to inspect the old buffer.
+    ;;  (while (get-buffer (concat "*" proc "*"))
+    ;;	(if (string= (substring proc -1) ">")
+    ;;	    (aset proc (- (length proc) 2) 
+    ;;		  (+ 1 (aref proc (- (length proc) 2))))
+    ;;	  (setq proc (concat proc "<2>"))))
+
+    ;; da: Finally removed this because it leads to objectionable 
     ;; proliferation of buffers when startup fails.
 
      ;; (while (get-buffer (concat "*" proc "*"))
@@ -461,7 +471,8 @@ so that loading them the next time round does not require re-processing."
   (proof-script-remove-all-spans-and-deactivate)
   (setq proof-included-files-list nil
 	proof-shell-busy nil
-	proof-shell-proof-completed nil)
+	proof-shell-proof-completed nil
+	proof-action-list nil)
   (if (and (buffer-live-p proof-shell-buffer)
 	   proof-shell-restart-cmd)
 	   (proof-shell-invisible-command
@@ -820,7 +831,7 @@ See the documentation for `proof-shell-delayed-output' for further details."
      ;;
      ;; 3. Nothing else should happen
      ;;
-     (t (assert nil))))
+     (t (assert nil "proof-shell-handle-delayed-output: wrong type!"))))
   (run-hooks 'proof-shell-handle-delayed-output-hook)
   (setq proof-shell-delayed-output (cons 'insert "done")))
 
@@ -899,21 +910,17 @@ Then we call `proof-shell-handle-error-hook'. "
 
 ;; FIXME da: this function is a mess.
 (defun proof-shell-handle-interrupt ()
-  (save-excursion 
-    (set-buffer proof-goals-buffer)
-    (display-buffer proof-goals-buffer)
-    (goto-char (point-max))
-    (newline 2)
-    (insert-string 
-     "Interrupt: Script Management may be in an inconsistent state\n")
-    (beep)
-    (if proof-script-buffer
-	(set-buffer proof-script-buffer)))
-  (if proof-shell-busy
-      (progn (proof-detach-queue)
-	     (setq proof-action-list nil)
-	     (delete-spans (proof-locked-end) (point-max) 'type)
-	     (proof-release-lock))))
+  (proof-shell-maybe-erase-response t t t)
+  (proof-warning 
+   "Interrupt: script management may be in an inconsistent state")
+  (beep)
+  (if (and proof-shell-busy proof-script-buffer)
+      (with-current-buffer proof-script-buffer
+	(proof-detach-queue)
+	;; FIXME: point-max seems a bit excessive here
+	(delete-spans (proof-locked-end) (point-max) 'type)))
+  (setq proof-action-list nil)
+  (proof-release-lock))
 
 (defun proof-goals-pos (span maparg)
   "Given a span, return the start of it if corresponds to a goal, nil otherwise."
@@ -1079,13 +1086,12 @@ particularly in proof-start-queue and proof-shell-exec-loop."
 
 ; Pass start and end as nil if the cmd isn't in the buffer.
 
-;; FIXME: note: removed optional 'relaxed' arg
-(defun proof-start-queue (start end alist)
-  "Begin processing a queue of commands in ALIST.
-If START is non-nil, START and END are buffer positions in the
-active scripting buffer for the queue region."
-  (if start
-      (proof-set-queue-endpoints start end))
+
+(defun proof-append-alist (alist &optional queuemode)
+  "Chop off the vacuous prefix of the command queue ALIST and queue it.
+For each proof-no-command item, at the head of the list, invoke its 
+callback and remove it from the list.
+Returns the possibly shortened list."
   (let (item)
     (while (and alist (string= 
 		       (nth 1 (setq item (car alist))) 
@@ -1093,11 +1099,36 @@ active scripting buffer for the queue region."
       (funcall (nth 2 item) (car item))
       (setq alist (cdr alist)))
     (if alist
-	(progn
-	  (proof-grab-lock) 
-	  (setq proof-shell-delayed-output (cons 'insert "Done."))
-	  (setq proof-action-list alist)
-	  (proof-shell-insert (nth 1 item))))))
+	(if proof-action-list
+	    (progn
+	      ;; internal check: correct queuemode in force
+	      (and queuemode (assert (eq proof-shell-busy queuemode)))
+	      ;; append to the current queue
+	      (setq proof-action-list
+		    (nconc proof-action-list alist)))
+	  ;; start processing a new queue
+	  (progn
+	    (proof-grab-lock queuemode) 
+	    (setq proof-shell-delayed-output (cons 'insert "Done."))
+	    (setq proof-action-list alist)
+	    (proof-shell-insert (nth 1 item)))))))
+    
+(defun proof-start-queue (start end alist)
+  "Begin processing a queue of commands in ALIST.
+If START is non-nil, START and END are buffer positions in the
+active scripting buffer for the queue region."
+  (if start
+      (proof-set-queue-endpoints start end))
+  (proof-append-alist alist))
+
+(defun proof-extend-queue (end alist)
+  "Extend the current queue with commands in ALIST, queue end END.
+To make sense, the commands should correspond to processing actions
+for processing a region from (buffer-queue-or-locked-end) to END.
+The queue mode is set to 'advancing"
+  (proof-set-queue-endpoints (proof-unprocessed-begin) end)
+  (proof-append-alist alist 'advancing))
+
 
 ; returns t if it's run out of input
 
diff --git a/generic/proof-toolbar.el b/generic/proof-toolbar.el
index 97a7359f..b72d2f4b 100644
--- a/generic/proof-toolbar.el
+++ b/generic/proof-toolbar.el
@@ -326,7 +326,7 @@ changed state."
 Move point if the end of the locked position is invisible."
   (interactive)
   (proof-toolbar-move
-   (goto-char (proof-unprocessed-begin))
+   (goto-char (proof-queue-or-locked-end)) ; was unprocessed-begin
    (proof-assert-next-command-interactive))
   (proof-toolbar-follow))