Add proof-output-tooltips option to turn off output highlighting for people who read or edit by waving mouse at text

4 files changed, 45 insertions, 9 deletions

diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index c9b22a3d..0eef35b8 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -3244,6 +3244,7 @@ goals and response windows to fit their contents.
 
 The default value is @code{nil}.
 @end defopt
+
 @c TEXI DOCSTRING MAGIC: proof-colour-locked
 @defopt proof-colour-locked 
 If non-nil, colour the locked region with @samp{@code{proof-locked-face}}.@*
@@ -3252,6 +3253,19 @@ on locked regions.
 
 The default value is @code{t}.
 @end defopt
+
+@c TEXI DOCSTRING MAGIC: proof-output-tooltips
+@defopt proof-output-tooltips 
+Non-nil causes Proof General to add tooltips for prover output.@*
+Hovers will be added when this option is non-nil.  Prover outputs
+can be displayed when the mouse hovers over the region that
+produced it and output is available (see @samp{@code{proof-full-annotation}}).
+If output is not available, the type of the output region is displayed.
+Changes of this option will not be reflected in already-processed 
+regions of the script.
+
+The default value is @code{t}.
+@end defopt
 @node User options
 @section User options
 @c Index entries for each option 'concept'
diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index 798dba89..526673ee 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -292,6 +292,7 @@ without adjusting window layout."
 (proof-deftoggle proof-sticky-errors)
 (proof-deftoggle proof-shell-quiet-errors)
 (proof-deftoggle proof-minibuffer-messages)
+(proof-deftoggle proof-output-tooltips)
 (proof-deftoggle proof-autosend-enable proof-autosend-toggle)
 (proof-deftoggle proof-fast-process-buffer)
 (proof-deftoggle proof-imenu-enable proof-imenu-toggle)
@@ -379,6 +380,10 @@ without adjusting window layout."
        :style toggle
        :selected proof-minibuffer-messages
        :help "Show progress messages in minibuffer"]
+      ["Output tooltips" proof-output-tooltips-toggle
+       :style toggle
+       :selected proof-output-tooltips
+       :help "Add tooltips for prover output"]
       ["Auto Raise" proof-auto-raise-toggle
        :style toggle
        :selected proof-auto-raise-buffers
diff --git a/generic/proof-script.el b/generic/proof-script.el
index ec1f05bf..b189e02c 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -727,7 +727,10 @@ also as the 'response property on the span.
 
 Optional argument MOUSEFACE means use the given face as a mouse highlight
 face, if it is a face, otherwise, if it is non-nil but not a face,
-do not add a mouse highlight.
+do not add a mouse highlight.  
+
+In any case, a mouse highlight and tooltip are only set if
+`proof-output-tooltips' is non-nil.
 
 Argument FACE means add 'face property FACE to the span."
   (let* ((output     (pg-last-output-displayform))
@@ -746,10 +749,11 @@ Argument FACE means add 'face property FACE to the span."
     (span-set-property newspan 'pghelp t)
     (span-set-property newspan 'response output)
 
-    (span-set-property newspan 'help-echo
-	(if (<= (length output) 2)
-	      (pg-span-name span)
-	    output))
+    (when proof-output-tooltips
+      (span-set-property newspan 'help-echo
+			 (if (<= (length output) 2)
+			     (pg-span-name span)
+			   output)))
 
     ;; Here's the message we used to show in minibuffer
     ;; when pg-show-hints was on:
@@ -765,7 +769,8 @@ Argument FACE means add 'face property FACE to the span."
     (if (or (facep mouseface)
 	    (setq mouseface
 		  (unless mouseface 'proof-mouse-highlight-face)))
-	(span-set-property newspan 'mouse-face mouseface))
+	(when proof-output-tooltips
+	  (span-set-property newspan 'mouse-face mouseface)))
     (if face
 	(span-set-property newspan 'face face))
     (span-set-property newspan 'priority 50)))
diff --git a/generic/proof-useropts.el b/generic/proof-useropts.el
index b18a63f9..690b8db7 100644
--- a/generic/proof-useropts.el
+++ b/generic/proof-useropts.el
@@ -348,11 +348,23 @@ signals to the remote host."
   :group 'proof-user-options)
 
 (defcustom proof-full-annotation t
-  "*Non-nil causes Proof General to add hovers for all proof commands.
+  "*Non-nil causes Proof General to record output for all proof commands.
 Proof output is recorded as it occurs interactively; normally if
 many steps are taken at once, this output is suppressed.  If this
-setting is used to enable it, the proof script will be annotated
-with full details."
+setting is used to enable it, the proof script can be annotated
+with full details.  See also `proof-output-tooltips' to enable
+automatic display of output on mouse hovers."
+  :type 'boolean
+  :group 'proof-user-options)
+
+(defcustom proof-output-tooltips t
+  "*Non-nil causes Proof General to add tooltips for prover output.
+Hovers will be added when this option is non-nil.  Prover outputs
+can be displayed when the mouse hovers over the region that
+produced it and output is available (see `proof-full-annotation').
+If output is not available, the type of the output region is displayed.
+Changes of this option will not be reflected in already-processed 
+regions of the script."
   :type 'boolean
   :group 'proof-user-options)