[isabelle-dev] jEdit: tooltips don't have proper size
makarius at sketis.net
Wed Nov 28 19:31:19 CET 2012
On Wed, 24 Oct 2012, Steffen Juilf Smolka wrote:
> 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.)
The remaining problem is this: Given the size of the inner GUI component,
one needs to produce the size of the enclosing window, without knowing the
size of the additional decorational components. If the window would be
visible, one could query that, but it cannot be made visible before
knowing its size (the user would see that first attempt).
More information about the isabelle-dev