diff options
| author | David Aspinall | 2009-09-20 22:05:54 +0000 |
|---|---|---|
| committer | David Aspinall | 2009-09-20 22:05:54 +0000 |
| commit | 71df9d8fbd6a47a251059725349c5cd8b9664589 (patch) | |
| tree | fdda8782780e268282eec78aa65934b808133aca /generic/proof-script.el | |
| parent | 48d90b7f3ff38e197586a80ea4131330be33ec27 (diff) | |
proof-script-clear-queue-spans-on-error: jump to start of error span
(if proof-follow-mode suggests following locked region)
Diffstat (limited to 'generic/proof-script.el')
| -rw-r--r-- | generic/proof-script.el | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index 8f30ec44..56aad21c 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -295,7 +295,8 @@ value of proof-locked span." (defun proof-script-clear-queue-spans-on-error (badspan) "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. +caused the error. Go to the start of it if `proof-follow-mode' is +'locked. This is a subroutine used in proof-shell-handle-{error,interrupt}." (let ((start (proof-locked-end)) @@ -303,6 +304,10 @@ This is a subroutine used in proof-shell-handle-{error,interrupt}." (infop (span-live-p badspan))) (proof-detach-queue) (when infop + (when (eq proof-follow-mode 'locked) + ;; jump to start of error: should this be configurable? + (goto-char (span-start badspan)) + (skip-chars-forward " \t\n")) (pg-set-span-helphighlights badspan 'proof-script-error-face 'underline)) |