Re: [isabelle] Emacs 23/PG 4 problems on Mac
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.
I see your point -- when "full annotation" is switched off, they're
only added for incrementally processed steps and won't be removed
from already processed portions of the script. It might be better
to have an option to prevent adding them altogether.
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.
You can also customize tooltip-delay and tooltip-short-delay.
Or use your finger to point at what you're reading, 8-).
I have set these two variables to a longer delay (5s) for now, which
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...
This is by poor/old design in the Emacs display engine, which
replaces (rather than merges) the mouse-over face with the
underlying one which doesn't work well with font lock. You see the
same thing in Emacs native modes, e.g. Info. I reported it as an
Emacs bug a while ago.
I have currently set the following variables
to the same color (lightblue in my case) as
In this way, the previous MTV-style flickering while moving the mouse
is reduced to the disappearing syntax highlighting, which I find less
Thank you all for your helpful hints.
This archive was generated by a fusion of
Pipermail (Mailman edition) and