diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2011-04-13 11:12:49 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2011-04-13 11:12:49 +0000 |
| commit | cb88c7236bf1d2aa276a62b7dfe0ef61a769f787 (patch) | |
| tree | d94d62bf03fc07c133c30c32144a92e45fb19bb5 /generic/proof-useropts.el | |
| parent | 48fe5f38679c0c99e446a4666199a6d5ab27190c (diff) | |
Add proof-output-tooltips option to turn off output highlighting for people who read or edit by waving mouse at text
Diffstat (limited to 'generic/proof-useropts.el')
| -rw-r--r-- | generic/proof-useropts.el | 18 |
1 files changed, 15 insertions, 3 deletions
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) |