Re: [isabelle] Emacs 23/PG 4 problems on Mac



3) When I point the mouse on a processed part of the input it becomes
highlighted in yellow and displays a "tooltip" frame with info about the
underlying object. Inside proofs it shows the proof state at the mouse
position. While this looks like a cool new feature in PG4, I would like to
be able to turn both the highlighting and the "tooltips" off, when I do not
need them. However, I was unable to find an option that achieves this.

I would also like to be able to turn this feature off.

Me, too... I get annoyed by this quite regularly.

On 04/12/2011 07:52 PM, David Aspinall wrote:
http://tinyurl.com/pgchap3

This didn't help me. As I understand it, switching off "Full Annotation" should prevent saving (and displaying) the prover output. But even when disabled, I still get the tooltips, and they normally sit right in front of the text I am trying to read, forcing me to move the mouse.

As a workaround, I discovered that turning off "tooltip-mode" removes the gigantic tooltips and instead displays the text in the minibuffer, which is less intrusive.

The yellow highlight can be removed by customizing the appropriate face. Unfortunately, the syntax highlighting of the normal text (foreground colour) still disappears on mouseover...

Alex





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.