diff options
| author | David Aspinall | 2010-08-17 11:54:02 +0000 |
|---|---|---|
| committer | David Aspinall | 2010-08-17 11:54:02 +0000 |
| commit | be0f8150a8f4ffaf9b284ea7dfd39c28612bf8ed (patch) | |
| tree | 1e8e57e94c5924296fb731420ac28ca07a8966ef /generic/proof-script.el | |
| parent | 865b7617135e442672725f9771a17e765488ccdf (diff) | |
Clean up handling of pending interrupts, remove experimental proof-shell-interrupts-after-commit.
Diffstat (limited to 'generic/proof-script.el')
| -rw-r--r-- | generic/proof-script.el | 15 |
1 files changed, 9 insertions, 6 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index 25c87e10..79fba2a0 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -308,12 +308,14 @@ value of proof-locked span." "Remove all spans from scripting buffers via `proof-restart-buffers'." (proof-restart-buffers (proof-script-buffers-with-spans))) -(defun proof-script-clear-queue-spans-on-error (badspan) +(defun proof-script-clear-queue-spans-on-error (badspan &optional interruptp) "Remove the queue span from buffer, cleaning spans no longer queued. If BADSPAN is non-nil, assume that this was the span whose command caused the error. Go to the start of it if `proof-follow-mode' is 'locked. +If INTERRUPTP is non-nil, do not consider BADSPAN itself as faulty. + This is a subroutine used in proof-shell-handle-{error,interrupt}." (let ((start (proof-unprocessed-begin)) (end (proof-queue-or-locked-end)) @@ -325,10 +327,11 @@ This is a subroutine used in proof-shell-handle-{error,interrupt}." ;; jump to start of error: should this be configurable? (goto-char (span-start badspan)) (skip-chars-forward " \t\n"))) - (when proof-sticky-errors - (pg-set-span-helphighlights badspan - 'proof-script-highlight-error-face - 'proof-script-sticky-error-face))) + (unless interruptp + (when proof-sticky-errors + (pg-set-span-helphighlights badspan + 'proof-script-highlight-error-face + 'proof-script-sticky-error-face)))) (proof-script-delete-spans start end))) (defun proof-script-delete-spans (beg end) @@ -372,7 +375,7 @@ This position should be the first writable position in the buffer. An appropriate point to move point to (or make sure is displayed) when a queue of commands is being processed." (or - ;; span-end returns nil if span is detatched + ;; span-end returns nil if span is detached (and proof-queue-span (span-end proof-queue-span)) (and proof-locked-span (span-end proof-locked-span)) (point-min))) |