Implement the eagerly anticipated Beyond Script Management Feature No.2 (i.e., automatic preview of next command)

5 files changed, 115 insertions, 46 deletions

diff --git a/generic/pg-user.el b/generic/pg-user.el
index 423521d0..35b015ad 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -1405,8 +1405,8 @@ assuming the undo-in-region behavior will apply if ARG is non-nil."
 
 (defvar proof-autosend-timer nil "Timer used by autosend.")
 
-(deflocal proof-autosend-error-point nil
-  "If auto-sending hits an error, records the point where it is.")
+(deflocal proof-autosend-modified-tick nil
+  "Records 'buffer-chars-modified-tick' since last autosend.")
 
 ;;;###autoload
 (defun proof-autosend-enable (&optional nomsg)
@@ -1430,21 +1430,20 @@ assuming the undo-in-region behavior will apply if ARG is non-nil."
 (defun proof-autosend-loop ()
   (proof-with-current-buffer-if-exists proof-script-buffer
     (unless (or (proof-locked-region-full-p)
-		proof-shell-busy)
-	(proof-autosend-loop-all))))
+		proof-shell-busy
+		(eq (buffer-chars-modified-tick) proof-autosend-modified-tick))
+      (setq proof-autosend-running t)
+      (setq proof-autosend-modified-tick (buffer-chars-modified-tick))
+      (if proof-autosend-all
+	  (proof-autosend-loop-all)
+	(proof-autosend-loop-next))
+      (setq proof-autosend-running nil))))
 
 (defun proof-autosend-loop-all ()
   "Send commands from the script until an error, complete, or input appears."
-  (when proof-autosend-error-point
-    (if (< proof-last-edited-low-watermark proof-autosend-error-point)
-	;; there was an edit before the error
-	;; FIXME: this isn't good enough, edit of the command which caused
-	;; the error, or earlier is what we want.  Need to record that.
-	(setq proof-autosend-error-point nil)))
-  (unless (or proof-autosend-error-point  
-	      (eq proof-shell-last-queuemode 'retracting))
+  (unless (eq proof-shell-last-queuemode 'retracting)
     (message "Sending commands to prover...")
-    (setq proof-autosend-running t)
+    (setq proof-autosend-modified-tick (buffer-chars-modified-tick))
     (unwind-protect
 	(progn
 	  (save-excursion
@@ -1465,15 +1464,51 @@ assuming the undo-in-region behavior will apply if ARG is non-nil."
 	    (message "Sending commands to prover...interrupted")
 	    (proof-shell-wait))
 	   (t
-	    (message "Sending commands to prover...done"))))
-      (setq proof-autosend-running nil))))
-
-;; TODO (see beyondsm)
-;(defun proof-autosend-loop-next ()
-;  "Send the next command from the script and indicate its success/otherwise"
+	    (message "Sending commands to prover...done")))))))
+
+(defun proof-autosend-loop-next ()
+  "Send the next command from the script and indicate its success/otherwise."
+  (unwind-protect
+      (let ((qol   (proof-queue-or-locked-end)))
+	(save-excursion
+	  ;(goto-char qol)
+	  ;(skip-chars-forward " \t\n")
+	  (message "Trying next command in prover...")
+	  (proof-assert-until-point
+	   (if proof-multiple-frames-enable 
+	       'no-minibuffer-messages ; nb: not API
+	     '(no-response-display 
+	       no-error-display
+	       no-goals-display))))
+	(let ((proof-sticky-errors t))
+	  (proof-shell-wait t)) ; interruptible
+	(cond
+	 ((eq proof-shell-last-output-kind 'error)
+	  (setq proof-autosend-error-point (proof-unprocessed-begin))
+	  (message "Trying next command in prover...error"))
+	 ((and (input-pending-p) proof-shell-busy)
+	  (proof-interrupt-process)
+	  (message "Trying next command in prover...interrupted")
+	  (proof-shell-wait))
+	 (t
+	  (message "Sending next command to prover...done")))
+	;; success: now undo in prover, but colour undone spans if OK
+	(unless (eq qol (proof-queue-or-locked-end)) ; no progress
+	  (save-excursion
+	    (goto-char qol)
+	    (proof-retract-until-point 
+	     (lambda (beg end)
+	       (span-add-self-removing-span 
+		(save-excursion
+		  (goto-char beg)
+		  (skip-chars-forward " \t\n")
+		  (point)) 
+		end
+		'face 'highlight))
+	     '(no-response-display 
+	       no-error-display
+	       no-goals-display)))))))
   
-
-
 (provide 'pg-user)
 
 ;;; pg-user.el ends here
diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index f9a4bc07..81b31a06 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -316,15 +316,7 @@ without adjusting window layout."
 (defconst proof-quick-opts-menu
   (cons
    "Quick Options"
-   `(["Electric Terminator" proof-electric-terminator-toggle
-     :style toggle
-     :selected proof-electric-terminator-enable
-     :help "Automatically send commands as typed"]
-     ["Send Automatically" proof-autosend-toggle
-      :style toggle
-      :selected proof-autosend-enable
-      :help "Automatically send commands when idle"]
-     ["Fast Process Buffer" proof-fast-process-buffer-toggle
+   `(["Fast Process Buffer" proof-fast-process-buffer-toggle
       :style toggle
       :selected proof-fast-process-buffer
       :help "Use a fast loop when processing whole buffer (disables input)"]
@@ -355,6 +347,28 @@ without adjusting window layout."
       :style toggle
       :selected (not proof-shell-quiet-errors)
       :help "Beep on errors or interrupts"]
+     ("Auto Process"
+      ["Electric Terminator" proof-electric-terminator-toggle
+       :style toggle
+       :selected proof-electric-terminator-enable
+       :help "Automatically send commands when terminator typed"]
+      ["Process Automatically" proof-autosend-toggle
+       :style toggle
+       :selected proof-autosend-enable
+       :help "Automatically send commands when idle"]
+      ("Automatic Processing Mode"
+       ["Next Command"
+	(customize-set-variable 'proof-autosend-all nil)
+       :style radio
+       :selected (eq proof-autosend-all nil)
+       :active proof-autosend-enable
+       :help "Automatically try out the next commmand"]
+       ["Send Whole Buffer"
+	(customize-set-variable 'proof-autosend-all t)
+	:style radio
+	:selected (eq proof-autosend-all t)
+	:active proof-autosend-enable
+	:help "Automatically send the whole buffer"]))
      ("Display"
       ["Unicode Tokens"
       (proof-unicode-tokens-toggle (if (boundp 'unicode-tokens-mode)
diff --git a/generic/proof-script.el b/generic/proof-script.el
index b0f35200..e97e313e 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -1990,7 +1990,7 @@ others)."
   (if (span-live-p span)
       (let ((start (span-start span))
 	    (end (span-end span))
-	    (kill (span-property span 'delete-me)))
+	    (killfn (span-property span 'remove-action)))
 	;; da: check for empty region seems odd here?
 	;; [prevents regions from being detached in set-locked-end]
 	(unless (proof-locked-region-empty-p)
@@ -2007,18 +2007,19 @@ others)."
 
 	(proof-script-delete-spans start end)
 	(span-delete span)
-	(if kill (kill-region start end))))
+	(if killfn (funcall killfn start end))))
   ;; State of scripting may have changed now
   (run-hooks 'proof-state-change-hook))
 
-(defun proof-setup-retract-action (start end proof-commands delete-region)
+(defun proof-setup-retract-action (start end proof-commands remove-action &optional 
+					 displayflags)
   "Make span from START to END which corresponds to retraction.
 Returns retraction action destined for proof shell queue, and make span.
 Action holds PROOF-COMMANDS and `proof-done-retracting' callback.
-Span deletion property set to flag DELETE-REGION."
+Span deletion property set to function REMOVE-ACTION."
   (let ((span (span-make start end)))
-    (span-set-property span 'delete-me delete-region)
-    (list (list span proof-commands 'proof-done-retracting))))
+    (span-set-property span 'remove-action remove-action)
+    (list (list span proof-commands 'proof-done-retracting displayflags))))
 
 
 (defun proof-last-goal-or-goalsave ()
@@ -2045,8 +2046,8 @@ Span deletion property set to flag DELETE-REGION."
 ;; It might be simpler to just use a single undo/forget
 ;; command, which is called in all cases.
 ;;
-(defun proof-retract-target (target delete-region)
-  "Retract the span TARGET and delete it if DELETE-REGION is non-nil.
+(defun proof-retract-target (target undo-action displayflags)
+  "Retract the span TARGET and apply UNDO-ACTION to undone region if non-nil.
 Notice that this necessitates retracting any spans following TARGET,
 up to the end of the locked region."
   (let ((end   (proof-unprocessed-begin))
@@ -2087,7 +2088,7 @@ up to the end of the locked region."
 			     start end
 			     (if (null span) nil ; was: proof-no-command
 			       (funcall proof-count-undos-fn span))
-			     delete-region)
+			     undo-action)
 		    end start))
 	  ;; Otherwise, start the retraction by killing off the
 	  ;; currently active goal.
@@ -2099,7 +2100,8 @@ up to the end of the locked region."
 	  (setq actions
 		(proof-setup-retract-action (span-start span) end
 					    (list proof-kill-goal-command)
-						    delete-region)
+						    undo-action
+						    displayflags)
 		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
@@ -2116,7 +2118,8 @@ up to the end of the locked region."
 	      (nconc actions (proof-setup-retract-action
 			      start end
 			      (funcall proof-find-and-forget-fn target)
-			      delete-region))))
+			      undo-action
+			      displayflags))))
 
     (proof-start-queue (min start end) (proof-unprocessed-begin) 
 		       actions 'retracting)))
@@ -2133,15 +2136,16 @@ If invoked outside a locked region, undo the last successfully processed
 command.  If called with a prefix argument (DELETE-REGION non-nil), also
 delete the retracted region from the proof-script."
   (interactive "P")
-  (proof-retract-until-point delete-region))
+  (proof-retract-until-point 
+   (if delete-region 'kill-region)))
 
-(defun proof-retract-until-point (&optional delete-region)
+(defun proof-retract-until-point (&optional undo-action displayflags)
   "Set up the proof process for retracting until point.
 In particular, set a flag for the filter process to call
 `proof-done-retracting' after the proof process has successfully
 reset its state.
-If DELETE-REGION is non-nil, delete the region in the proof script
-corresponding to the proof command sequence.
+If UNDO-ACTION is non-nil, call this function on the region in
+the proof script corresponding to the proof command sequence.
 If invoked outside a locked region, undo the last successfully processed
 command."
   (if (proof-locked-region-empty-p)
@@ -2165,7 +2169,7 @@ command."
 	  (backward-char)
 	  (setq span (span-at (point) 'type)))
 	(if span
-	  (proof-retract-target span delete-region)
+	    (proof-retract-target span undo-action displayflags)
 	  ;; something wrong
 	  (proof-debug
 	   "proof-retract-until-point: couldn't find a span!"))))))
diff --git a/generic/proof-useropts.el b/generic/proof-useropts.el
index de4011cd..f1019217 100644
--- a/generic/proof-useropts.el
+++ b/generic/proof-useropts.el
@@ -386,6 +386,11 @@ are distracting or too frequent."
   :set 'proof-set-value
   :group 'proof-user-options)
 
+(defcustom proof-autosend-all nil
+  "*If non-nil, auto send will process whole buffer; otherwise just the next command."
+  :type 'boolean
+  :group 'proof-user-options)
+
 (defcustom proof-fast-process-buffer (featurep 'ns)
   "*If non-nil, `proof-process-buffer' will use a busy wait to process.
 This results in faster processing, but disables simultaneous user interaction."
diff --git a/lib/span.el b/lib/span.el
index 32967c78..6b576b87 100644
--- a/lib/span.el
+++ b/lib/span.el
@@ -215,6 +215,17 @@ Return nil if no such overlay belong to the list."
   "Set the end point of SPAN to VALUE."
   (span-set-endpoints span (span-start span) value))
 
+;;
+;; Handy overlay utils
+;;
+
+(defun span-add-self-removing-span (beg end &rest props)
+  (let ((ol (make-overlay beg end)))
+    (while props
+      (overlay-put ol (car props) (cadr props))
+      (setq props (cddr props)))
+    (add-timeout 2 'delete-overlay ol)))
+
 
 (provide 'span)