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

First the running gag on isabelle-dev: "the new ..." or "the latest ..." 
is ill-defined.  You have to refer to *the* changeset of the repository 
version you are presently testing.

Nonetheless, I can guess what you mean and to which version range it might 
refer: something close to my own latest version of my laptop, which is 
8b50286c36d3.  (This reference here is important for the mail archive of 
the list, because in some weeks or months nobody remembers what was 
current in the past.)


These fine points of sizing the Rich_Text_Area are not fully worked out 
yet, and the next release is still many weeks ahead.

I will take your observation is a slight increase of the priority to 
address it before the release, but this is not sure since many really 
important things still need to happen elsewhere.


Concerning "Source Code Pro" font: I tried it some weeks ago when there 
was an announcement somewhere, but dismissed it rather quickly.  On 
JVM/Linux its rendering quality appeared quite weak, and too many of our 
standard Isabelle symbols are missing.  (This can be checked by opening 
$ISABELLE_HOME_USER/etc/symbols with UTF-8-Isabelle encoding.)


 	Makarius