From 71df9d8fbd6a47a251059725349c5cd8b9664589 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Sun, 20 Sep 2009 22:05:54 +0000
Subject: proof-script-clear-queue-spans-on-error: jump to start of error span
 (if proof-follow-mode suggests following locked region)

---
 generic/proof-script.el | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

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))
-- 
cgit v1.2.3