[isabelle-dev] jEdit: tooltips don't have proper size
makarius at sketis.net
Sat Oct 27 16:42:18 CEST 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...
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.)
More information about the isabelle-dev