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

[Steffen Juilf Smolka]

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

Best Regards
Steffen