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

1 files changed, 14 insertions, 0 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'