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

[Makarius]

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).


 	Makarius