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

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

 - D.

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

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