From cb88c7236bf1d2aa276a62b7dfe0ef61a769f787 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Wed, 13 Apr 2011 11:12:49 +0000 Subject: Add proof-output-tooltips option to turn off output highlighting for people who read or edit by waving mouse at text --- doc/ProofGeneral.texi | 14 ++++++++++++++ 1 file changed, 14 insertions(+) (limited to 'doc') diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index c9b22a3d..0eef35b8 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -3244,12 +3244,26 @@ 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}}.@* If this is not set, buffers will have no special face set 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 -- cgit v1.2.3