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
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.
Sorry, I'll keep that in mind.
Concerning Source Code Pro font: I tried it some weeks ago when there was
an
Hi,
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
