[isabelle-dev] jEdit: tooltips don't have proper size
Steffen Juilf Smolka
steffen.smolka at in.tum.de
Wed Nov 28 20:25:11 CET 2012
>> 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.
More information about the isabelle-dev