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

8 files changed, 96 insertions, 34 deletions

diff --git a/CHANGES b/CHANGES
index 28dfbe11..db67878e 100644
--- a/CHANGES
+++ b/CHANGES
@@ -4,7 +4,7 @@
 
 ** Isabelle/Isar changes
 
-*** Electric terminator works, without inserting terminator
+*** Electric terminator works without inserting terminator
 
 
 ** Generic changes
@@ -13,8 +13,18 @@
 
 *** Font-lock based Unicode Tokens mode replaces X-Symbol
 
+*** Output retained for script buffer popups
+    Depending on input language and interaction output, this
+    may enable a "script centred" way of working, when output
+    buffers can be ignored and hidden.  Disable auto raise for this.
+    Use full decoration to keep output when several steps are taken.
+
+*** New user configuration options
+    proof-auto-raise-buffers  (set to nil for manual control)
+    proof-full-decoration     (add full decoration to input)
+
 *** Removed user configuration options
-    proof-toolbar-use-button-enablers  (now always enabled)
+    proof-toolbar-use-button-enablers  (now always used)
 
 *** Altered prover configuration settings
     pg-insert-output-as-comment-fn:  removed
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 4fe293e3..2d46d2b0 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -2656,12 +2656,13 @@ For more help with customize, see @inforef{Customization, ,(emacs)}.
 @cindex frames
 @cindex multiple frames
 @cindex three-buffer interaction
+@cindex auto raise
 
 By default, Proof General displays two buffers during scripting, in a
 split window on the display.  One buffer is the script buffer.  The
-other buffer is either the goals buffer (e.g. @code{*isabelle-goals*})
-or the response buffer (@code{*isabelle-response*}).  Proof General
-switches between these last two automatically.  
+other buffer is either the goals buffer (@code{*goals*}) or the response
+buffer (@code{*response*}).  Proof General raises and switches between
+these last two automatically.  
 
 Proof General allows several ways to customize this default display
 model, by splitting the Emacs frames in different ways and maximising
@@ -2673,13 +2674,17 @@ on the menu:
 @end lisp
 and you can save your preferred default. 
 
-
 If your screen is large enough, you may prefer to display all three of
 the interaction buffers at once.  This is useful, for example, to see
 output from the @code{proof-find-theorems} command at the same time as
 the subgoal list.  Set the user option @code{proof-three-window-enable} to
 make Proof General keep both the goals and response buffer displayed.
 
+If you prefer to switch windows and buffers manually when you want to
+see the prover output, you can customize the user option
+@code{proof-auto-raise-buffers} to prevent the automatic behaviour.
+
+
 @c TEXI DOCSTRING MAGIC: proof-three-window-enable
 @defopt proof-three-window-enable 
 Whether response and goals buffers have dedicated windows.@*
@@ -2772,6 +2777,7 @@ For multiple frame mode, this function obeys the setting of
 @samp{@code{pg-response-eagerly-raise}}, which see.
 @end deffn
 
+@c  TEXI DOCSTRING MAGIC: proof-auto-raise-buffers
 
 @node User options
 @section User options
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.