diff options
-rw-r--r-- | doc/ProofGeneral.texi | 14 | ||||
-rw-r--r-- | generic/proof-menu.el | 5 | ||||
-rw-r--r-- | generic/proof-script.el | 17 | ||||
-rw-r--r-- | generic/proof-useropts.el | 18 |
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) |