Add proof state hover messages to proof script, along with useful customization.

6 files changed, 74 insertions, 28 deletions

diff --git a/generic/pg-response.el b/generic/pg-response.el
index c416843c..d97d58d5 100644
--- a/generic/pg-response.el
+++ b/generic/pg-response.el
@@ -165,7 +165,7 @@ For multiple frame mode, this function obeys the setting of
 	(switch-to-buffer proof-script-buffer))
     (proof-map-buffers (proof-associated-buffers)
       (if pg-response-eagerly-raise
-	  (proof-display-and-keep-buffer (current-buffer))))
+	  (proof-display-and-keep-buffer (current-buffer) nil 'force)))
     ;; Restore an existing frame configuration (seems buggy, typical)
     (if pg-frame-configuration
 	(set-frame-configuration pg-frame-configuration 'nodelete)))
@@ -180,7 +180,7 @@ For multiple frame mode, this function obeys the setting of
     (set-window-dedicated-p (selected-window) nil)
     (delete-other-windows)
     (if (buffer-live-p proof-response-buffer)
-	(proof-display-and-keep-buffer proof-response-buffer))))
+	(proof-display-and-keep-buffer proof-response-buffer nil 'force))))
   (pg-hint (pg-response-buffers-hint)))
 
 (defun proof-delete-other-frames ()
diff --git a/generic/proof-config.el b/generic/proof-config.el
index 258d501b..87b36e2f 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -238,6 +238,14 @@ goals and response windows to fit their contents."
   :type 'boolean
   :group 'proof-user-options)
 
+(defcustom proof-auto-raise-buffers t
+  "*If non-nil, automatically raise buffers to display latest output.
+If this is not set, buffers and windows will not be managed by
+Proof General."
+  :type 'boolean
+  :group 'proof-user-options)
+
+
 (defcustom proof-query-file-save-when-activating-scripting
   t
 "*If non-nil, query user to save files when activating scripting.
@@ -404,6 +412,16 @@ signals to the remote host."
   :type 'boolean
   :group 'proof-user-options)
 
+;; TODO: add doc
+(defcustom proof-full-decoration nil
+  "*Non-nil causes Proof General to add hovers for all proof commands.
+Proof output is recorded as it occurs interactively; normally if
+many steps are taken at once, this output is surpressed.  If this
+setting is used to enable it, the proof script will be annotated
+with full details."
+  :type 'boolean
+  :group 'proof-user-options)
+
 
 
 
diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index 7599f005..2cb4b60a 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -261,6 +261,7 @@ without adjusting window layout."
 (proof-deftoggle proof-shrink-windows-tofit)
 (proof-deftoggle proof-multiple-frames-enable proof-multiple-frames-toggle)
 (proof-deftoggle proof-three-window-enable proof-three-window-toggle)
+(proof-deftoggle proof-auto-raise-buffers proof-auto-raise-toggle)
 (proof-deftoggle proof-disappearing-proofs)
 (proof-deftoggle proof-strict-read-only)
 
@@ -295,6 +296,10 @@ without adjusting window layout."
       :style toggle
       :selected proof-script-fly-past-comments
       :help "Coalesce and skip over successive comments"]
+     ["Full Decoration" proof-full-decoration-toggle
+      :style toggle
+      :selected proof-full-decoration
+      :help "Record full information to decorate scripts (may cause slowdown)"]
      ["Disppearing Proofs" proof-disappearing-proofs-toggle 
       :style toggle
       :selected proof-disappearing-proofs
@@ -360,11 +365,13 @@ without adjusting window layout."
       :help "Use a navigation window (Speedbar)"]
 
      ("Display"
-      ["Layout Windows" proof-layout-windows
-       :help "Rearrange windows on the screen"]
+      ["Auto Raise" proof-auto-raise-toggle
+       :style toggle
+       :selected proof-auto-raise-buffers
+       :help "Automatically raise buffers when output arrives"]
       ["Use Three Panes" proof-three-window-toggle
-       :active (not proof-multiple-frames-enable)
        :style toggle
+       :active (not proof-multiple-frames-enable)
        :selected proof-three-window-enable
        :help "Use three panes"]
       ;; We use non-Emacs terminology "Windows" in this menu to help
@@ -440,6 +447,7 @@ without adjusting window layout."
    'proof-electric-terminator-enable
    'proof-script-fly-past-comments
    'proof-disappearing-proofs 
+   'proof-full-decoration
    ;;'proof-output-fontify-enable
    'proof-strict-read-only
    (proof-ass-sym unicode-tokens-enable)
@@ -449,6 +457,7 @@ without adjusting window layout."
    'proof-keep-response-history
    'proof-imenu-enable
    ;; Display sub-menu
+   'proof-auto-raise-buffers
    'proof-three-window-enable
    'proof-delete-empty-windows
    'proof-multiple-frames-enable
diff --git a/generic/proof-script.el b/generic/proof-script.el
index b3d1fb3d..d4e91b62 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -316,8 +316,7 @@ will deactivated."
 	   (with-current-buffer buffer
 	     (if proof-active-buffer-fake-minor-mode
 		 (setq proof-active-buffer-fake-minor-mode nil))
-	     (span-delete-spans (point-min) (point-max) 'type)  ;; remove top-level spans
-	     (span-delete-spans (point-min) (point-max) 'idiom) ;; and embedded spans
+	     (proof-script-delete-spans (point-min) (point-max))
 	     (setq pg-script-portions nil)		   ;; also the record of them
 	     (proof-detach-queue)	                   ;; remove queue and locked
 	     (proof-detach-locked)
@@ -348,8 +347,13 @@ This is a subroutine used in proof-shell-handle-{error,interrupt}."
 	(proof-detach-queue)
 	;; FIXME da: point-max seems a bit excessive here,
 	;; proof-queue-or-locked-end should be enough.
-	(span-delete-spans (proof-locked-end) (point-max) 'type))))
+	(proof-script-delete-spans (proof-locked-end) (point-max)))))
 
+(defun proof-script-delete-spans (beg end)
+  (span-delete-spans beg end 'type)
+  (span-delete-spans beg end 'idiom)
+  (span-delete-spans beg end 'pghelp))
+  
 
 
 
@@ -693,26 +697,40 @@ NAME does not need to be unique."
       map)
     "Keymap for the span context menu.")
 
-
 ;;;###autoload
 (defun pg-set-span-helphighlights (span &optional nohighlight)
-  "Set the help echo message, default highlight, and keymap for SPAN."
-  (let ((helpmsg (concat (pg-span-name span) ""))) ;;   " region"
-    (span-set-property span 'balloon-help helpmsg)
+  "Add a daughter help span for SPAN with help message, highlight, actions"
+  (let ((helpmsg    (pg-span-name span))
+	(proofstate (proof-shell-strip-output-markup
+		     (if unicode-tokens-mode
+			 (unicode-tokens-encode-str proof-shell-last-output)
+		       proof-shell-last-output)))
+	(newspan    (let ((newstart (save-excursion
+				      (goto-char (span-start span))
+				      (skip-chars-forward " \n\t")
+				      (point))))
+		      (span-make newstart (span-end span)))))
+    ;; NOTE: hack for Isabelle which puts ugly leading \n's in proofstate.
+    (if (eq (string-match "^\n" proofstate) 0)
+	(setq proofstate (substring proofstate 1)))
+    (setq helpmsg
+	  (concat (if (> (length proofstate) 2) "" helpmsg) 
+		  proofstate))
+    (span-set-property newspan 'pghelp t)
     (if pg-show-hints ;; only message in minibuf if hints on
 	(span-set-property
-	 span 'help-echo
-	 (substitute-command-keys
-	  (concat
+	 newspan 'help-echo
 	   helpmsg
-	   " ("
-	   (if (span-property span 'idiom)
-	       "with point in region, \\[pg-toggle-visibility] to show/hide; ")
-	   "\\<pg-span-context-menu-keymap>\\[pg-span-context-menu]"
-	   " for menu)"))))
-    (span-set-property span 'keymap pg-span-context-menu-keymap)
+	   ;; " ("
+	   ;; (substitute-command-keys
+	   ;;  (if (span-property span 'idiom)
+	   ;; 	"with point in region, \\[pg-toggle-visibility] to show/hide; "
+	   ;;    "\\<pg-span-context-menu-keymap>\\[pg-span-context-menu]"))
+	   ;; " for menu)")))
+	   ))
+    (span-set-property newspan 'keymap pg-span-context-menu-keymap)
     (unless nohighlight
-      (span-set-property span 'mouse-face 'proof-mouse-highlight-face))))
+      (span-set-property newspan 'mouse-face 'proof-mouse-highlight-face))))
 
 
 
@@ -2280,8 +2298,7 @@ others)."
 ;; 			 (span-property span 'cmd))))))
 ;; 	  (mapcar fn (reverse cmds)))
 	
-	(span-delete-spans start end 'type)
-	(span-delete-spans start end 'idiom)
+	(proof-script-delete-spans start end)
 	(span-delete span)
 	(if kill (kill-region start end))))
   ;; State of scripting may have changed now
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 30b430c5..43ca29d9 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -931,7 +931,8 @@ track what happens in the proof queue."
 ;; FIXME: could be macro for efficiency improvement in avoiding calculating num
 (defun proof-shell-should-be-silent (num)
   "Return non-nil if we must switch to silent mode, adding NUM entries to queue."
-  (if proof-shell-start-silent-cmd
+  (if (and (not proof-full-decoration)
+	   proof-shell-start-silent-cmd)
       (or proof-shell-silent	; already
 	  ;; NB: there is some question here over counting the
 	  ;; proof-action-list, since it could itself contain
diff --git a/generic/proof-utils.el b/generic/proof-utils.el
index 9e5ca52c..faf76474 100644
--- a/generic/proof-utils.el
+++ b/generic/proof-utils.el
@@ -408,12 +408,13 @@ NB: may change the selected window."
   ;; Return the window, hopefully the one we first thought of.
   (get-buffer-window buffer 0))
 
-(defun proof-display-and-keep-buffer (buffer &optional pos)
+(defun proof-display-and-keep-buffer (buffer &optional pos force)
   "Display BUFFER and make window according to display mode.
 If optional POS is present, will set point to POS.
 Otherwise move point to the end of the buffer.
 Ensure that point is visible in window."
-  (save-excursion
+  (if (or force proof-auto-raise-buffers)
+    (save-excursion
     (save-selected-window
       (let ((window (proof-get-window-for-buffer buffer)))
 	(if (window-live-p window) ;; [fails sometimes?]
@@ -447,7 +448,7 @@ Ensure that point is visible in window."
                     (unless mode-line-format
                       ;; If the buffer gets displayed elsewhere, re-add
                       ;; the modeline.
-                      (kill-local-variable 'mode-line-format)))))))))))
+                      (kill-local-variable 'mode-line-format))))))))))))
 
 (defun proof-clean-buffer (buffer)
   "Erase buffer and hide from display if proof-delete-empty-windows set.