By default, do not move pointer on interrupt, only error; tune hints for spans

3 files changed, 42 insertions, 8 deletions

diff --git a/generic/pg-user.el b/generic/pg-user.el
index bf311ebb..28fd12ec 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -1001,6 +1001,9 @@ If NUM is negative, move upwards.  Return new span."
    (format
     "Use \\[proof-prf] to display goals; \\[proof-display-some-buffers] to rotate output %s"
     (if nextbuf (concat "(next: " nextbuf ")") ""))))
+
+(defun pg-jump-to-end-hint ()
+  (pg-hint "Use \\[proof-goto-end-of-locked] to jump to end of processed region"))
   
 (defun pg-processing-complete-hint ()
   "Display hint for showing end of locked region or processing complete."
@@ -1016,8 +1019,7 @@ If NUM is negative, move upwards.  Return new span."
 	      (pg-hint 
 	       (concat "Processing complete in " (buffer-name proof-script-buffer))))
 	     (t ;; partly complete: hint about displaying the locked end
-	      (pg-hint
-	       "Use \\[proof-goto-end-of-locked] to display end of locked region"))))))))
+	      (pg-jump-to-end-hint))))))))
 
 (defun pg-hint (hintmsg)
   "Display a hint HINTMSG in the minibuffer, if `pg-show-hints' is non-nil.
diff --git a/generic/proof-config.el b/generic/proof-config.el
index 43ed5098..5fdb7322 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -2148,10 +2148,17 @@ its friends configured in the function proof-shell-start."
   :group 'proof-shell)
 
 (defcustom proof-shell-handle-error-or-interrupt-hook
-  '(proof-goto-end-of-locked-if-pos-not-visible-in-window)
+  '(proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window)
   "Run after an error or interrupt has been reported in the response buffer.
 Hook functions may inspect `proof-shell-error-or-interrupt-seen' to 
-determine whether the cause was an error or interrupt."
+determine whether the cause was an error or interrupt.  Possible
+values for this hook include:
+
+ proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window
+ proof-goto-end-of-locked-if-pos-not-visible-in-window
+
+which move the cursor in the scripting buffer on an error or
+error/interrupt."
   :type '(repeat function)
   :group 'proof-shell)
 
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 76008f11..a78349c6 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -451,7 +451,7 @@ If interactive or SWITCH is non-nil, switch to script buffer first."
 ;; Careful: movement can happen when the user is typing, not very nice!
 (defun proof-goto-end-of-locked-if-pos-not-visible-in-window ()
   "If the end of the locked region is not visible, jump to the end of it.
-A possible hook function for proof-shell-handle-error-or-interrupt-hook.
+A possible hook function for `proof-shell-handle-error-or-interrupt-hook'.
 Does nothing if there is no active scripting buffer, or if
 `proof-follow-mode' is set to 'ignore."
   (interactive)
@@ -463,6 +463,20 @@ Does nothing if there is no active scripting buffer, or if
 	(unless (and win (pos-visible-in-window-p pos))
 	  (proof-goto-end-of-locked t)))))
 
+(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window ()
+  "As `proof-goto-end-of-locked-if-pos-not-visible-in-window' except not for interrupts.
+Intended as a hook function for `proof-shell-handle-error-or-interrupt-hook'."
+  (interactive)
+  (cond
+   ((eq proof-shell-error-or-interrupt-seen 'error)
+    (proof-goto-end-of-locked-if-pos-not-visible-in-window))
+   ((eq proof-shell-error-or-interrupt-seen 'interrupt)
+    (proof-with-current-buffer-if-exists 
+     proof-script-buffer
+     (pg-jump-to-end-hint)))))
+    
+
+
 ;; Simplified version of above for toolbar follow mode -- which wouldn't
 ;; work with abouve because of proof-shell-handle-error-or-interrupt-hook[?]
 (defun proof-goto-end-of-queue-or-locked-if-not-visible ()
@@ -656,7 +670,9 @@ NAME does not need to be unique."
     (cond 
      (idiom
       (concat (upcase-initials (symbol-name idiom))
-	      (if name (concat ": " name))))
+	      (if (and name 
+		       (not (equal name proof-unnamed-theorem-name)))
+		  (concat "[" name "]"))))
      ((or (eq type 'proof) (eq type 'goalsave))
       (concat "Proof" 
 	      (let ((name (span-property span 'name)))
@@ -669,9 +685,18 @@ NAME does not need to be unique."
 
 (defun pg-set-span-helphighlights (span &optional nohighlight)
   "Set the help echo message, default highlight, and keymap for SPAN."
-  (let ((helpmsg (pg-span-name span)))
+  (let ((helpmsg (concat (pg-span-name span) " region")))
     (set-span-property span 'balloon-help helpmsg)
-    (set-span-property span 'help-echo helpmsg)
+    (if pg-show-hints ;; only message in minibuf if hints on
+	(set-span-property 
+	 span 'help-echo 
+	 (concat helpmsg
+		 (substitute-command-keys
+		  (concat
+		   " (use "
+		   (if (span-property span 'idiom)
+		       "\\[pg-toggle-visibility] to show/hide; ")
+		       "\\[popup-mode-menu] for menu)")))))
     (set-span-property span 'keymap pg-span-context-menu-keymap)
     (unless nohighlight
       (set-span-property span 'mouse-face 'proof-mouse-highlight-face))))