[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...
More information about the isabelle-dev