[isabelle-dev] jEdit: tooltips don't have proper size

[Steffen Juilf Smolka]

>> It seems there is a little (but annoying) issue with the new tooltips in Isabelle/jEdit when using a font other than IsabelleText. I'm using the Source Code Pro font and the tooltips are always just a little too small so that part of the text is hidden/cut off. Of course an easy fix would be to go back to using IsabelleText...
> 
> Did you try this again?
> 
> Last week I've refined it a little bit, in the vicinity of Isabelle/4f2b5b2a9ad5.  It is a bit better, but not really precise, just some heuristics that I've tried with the 5 most common fonts that I know of, and a range of font sizes.  (I am still not convinced of Source Code Pro at all, despite its name and the marketing they made some weeks ago.)

I just tried it, and it now works perfectly with Source Code Pro.
Awesome, thanks! 

Steffen