diff options
-rw-r--r-- | generic/pg-user.el | 77 | ||||
-rw-r--r-- | generic/proof-menu.el | 32 | ||||
-rw-r--r-- | generic/proof-script.el | 36 | ||||
-rw-r--r-- | generic/proof-useropts.el | 5 | ||||
-rw-r--r-- | lib/span.el | 11 |
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) |