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

Steffen Juilf Smolka steffen.smolka at in.tum.de
Wed Oct 24 17:03:15 CEST 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...

Best Regards

More information about the isabelle-dev mailing list