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.

Exactly.


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 helps.


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

 proof-command-mouse-highlight-face
 proof-mouse-highlight-face
 proof-region-mouse-highlight-face

to the same color (lightblue in my case) as

 proof-locked-face

In this way, the previous MTV-style flickering while moving the mouse is reduced to the disappearing syntax highlighting, which I find less distracting.

Thank you all for your helpful hints.

Best,
Christoph













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