Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Funny font metrics in the Search and Replace d...


view this post on Zulip Email Gateway (Aug 22 2022 at 12:19):

From: Clemens Ballarin <ballarin@in.tum.de>
The font metrics in the Search and Replace dialog has been funny for a while, and this is still the case with RC2's versions of jdk, jedit and fonts. In the attached screenshot, the entire text is selected but the last 2 1/2 characters are not covered by the box.

MacBook Pro (Retina, 13-inch, Early 2015) and OS X 10.10.5.

Not sure this is something under our control, though.

Clemens
Screen Shot 2016-01-26 at 22.43.46.png

view this post on Zulip Email Gateway (Aug 22 2022 at 12:19):

From: Makarius <makarius@sketis.net>
Is that Isabelle/jEdit in the default configuration?

There should be the IsabelleText font in the main text area, as well as in
the small text field of the search dialog. jEdit plays some special
tricks to achieve that.

In the screenshot the font in the text field is a different one: it looks
more like the default one by Apple.

Makarius

view this post on Zulip Email Gateway (Aug 22 2022 at 12:21):

From: Makarius <makarius@sketis.net>
The key parameter is the main text area font. IsabelleText (in any size)
should be fine.

jEdit pokes into look-and-feel defaults to achieve the trick, e.g. try
this in the Scala console:

view.getTextArea.getPainter.getFont
javax.swing.UIManager.getDefaults().get("TextArea.font")

The first is the jEdit text area font, the second the font of Swing text
areas, as in the search dialog.

It should give the same font.

Or maybe you have an old version of that font installed on the system? An
effect of that might be missing glyphs in the NEWS file or the Symbols /
Document panel: various new symbol interpretations have been added for
Isabelle2016.

Another source of problem could be the Retina display: I don't have that
and can't test it.

Makarius

view this post on Zulip Email Gateway (Aug 22 2022 at 12:21):

From: Makarius <makarius@sketis.net>
On Thu, 28 Jan 2016, Clemens Ballarin wrote:

They give the same font:

scala> view.getTextArea.getPainter.getFont
res0: java.awt.Font = java.awt.Font[family=IsabelleText,name=IsabelleText,style=plain,size=14]

scala> javax.swing.UIManager.getDefaults().get("TextArea.font")
res1: Object = java.awt.Font[family=IsabelleText,name=IsabelleText,style=plain,size=14]

Does that also produce the same font?

(new javax.swing.JTextArea).getFont

Another source of problem could be the Retina display: I don't have
that and can't test it.

If I choose some other font for the text area (such as Courier) that
get's displayed both in the main text area and the search dialog. Now
the only thing special about IsabelleText (that I can imagine) that its
not installed in the system. It tried to verify this but FontBook
cannot open *.sfd files, so I couldn't install them...

The .sfd files are the sources for fontforge. The TrueType fonts are
Isabelle2016-RC2/contrib/isabelle_fonts-20160102

As a test it is fine to install them on the system, but don't forget to
remove them later.

There could be also something wrong with the generated .ttf fonts by
fontforge: it has many parameters, and some could be wrong for Mac OS X
with Retina.

Makarius

view this post on Zulip Email Gateway (Aug 22 2022 at 12:23):

From: Makarius <makarius@sketis.net>
What is missing in the main text area is proper bold. Hopefully this will
display correctly after installing IsabelleTextBold as well. (Otherwise
we are back to strange Apple/Java font rendering problems from Java 6.)

I am also puzzled that no other OSX Retina user has seen this problem
before (or seen and not reported).

Makarius

view this post on Zulip Email Gateway (Aug 22 2022 at 12:49):

From: Makarius <makarius@sketis.net>
In the meantime I've had a chance to look at 2-3 Macs with Retina. The
problem occurs both for Isabelle2015 (with Java 7) and Isabelle2016-RC3
(with Java 8).

Depending on the point size of the main text area, the deviation in the
text field (e.g. Search dialog) varies. Sometimes it is hardly visible at
all.

Conclusion for this release: it is not a regression so there are no
further attempts to finish the work of Apple and Oracle. Instead there is
a bit of documentation in the Isabelle/jEdit manual:
https://bitbucket.org/isabelle_project/isabelle-release/commits/dfb70abaa3f0

Makarius


Last updated: Mar 28 2024 at 08:18 UTC