Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New release, fonts


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

From: "John F. Hughes" <jfh@cs.brown.edu>
TL;DR: Never give a multiple-choice quiz where there's only one answer.

I partly agree with Peter and Eugene here (about the new fonts). I'm using
a QHD-wide "27 inch" display, and the new fonts look blurry, and also look
as if they're mostly bold; almost all text resembles the old bolded-keyword
look. Just to be sure it wasn't merely the display, I looked at the same
thing on my MacBook's 15" display --- same results.) The new bold keywords
are even more bold, but appear blurrier to me (and my eyesight isn't that
great -- for someone with clear vision, I'd expect this to be even more of
a problem). By contrast, the old ones look crisp (esp. for the material
within double-quotes). I far prefer them.

I did a screen grab of the two, side-by-side, and dropped it here:
https://imgur.com/a/3htvAfu; if you zoom in a bit and look at, for
instance, 'a, you'll see that the quote mark is far more blurry; look at
the "n" in "fun" and notice the blurry right-hand side. That certainly
explains what I was seeing/feeling. I love me some antialiasing, but ...
sometimes the results are unsatisfactory.

Is this a drop-dead issue for me the way it is for Eugene? Probably not.
But I think you should consider what Eugene and Peter say, not spend time
explaining why the technology is the way it is. (FYA, see
https://www.youtube.com/watch?v=dEP7aEyTOf0, 0:34 - 0:55).

As for "old technology", if you go look for monitors on Amazon or similar
places, you'll find that most high-end screens are about 100 DPI which, for
displays at comparable distances, is really the relevant measure. My "27
inch" display (23 inches wide) is 2560 pixels; the top-rated UHD display on
Amazon is about 33 inches wide and 3340 pixels. (To be fair, also top-rated
is a 25 inch display with 3340 pixels -- about 5/4 the DPI of my display.)
So what Eugene is describing is hardly old-school in terms of actual size
of pixels-at-the-cornea (assuming that like most folks I know, Eugene has
the display about 24-30" inches away, and has had it that way through
multiple generations of resolution-improvement).

The sidekick is an interesting case; I can't figure out how to make the
font larger in I2018, so it's not a fair comparison, but with the default
install of I2019 on my Mac, the wide-bold does lead to some serious
ugliness. Look at the space between "theory" and "Seq": in the old
sidekick, it's clearly a blank space. In the new one, it's much narrower
and harder to recognize. It's also not clear why, among the main-text
panel, the upper sidekick panel, and the lower sidekick panel, this one
alone has a non-fixed-width font.

There's one place where I feel the new is a definite improvement on the
old: opening and closing parentheses. You can see this in the comment in
the first two lines. The old one looks threadbare, while the new appears
more like a uniform-thickness stroke.

If your chosen font/renderer makes things appear ugly to folks, and they
tell you so, then your pre-release testing is a success: you're getting
useful feedback (which is a precious resource). As someone with a bit of
experience in graphics and UIs, I'd advise you to not ignore or dismiss it
if you care about the graphics and UI. Feel free, of course, to ignore
me. I suspect that this is not your top concern in an otherwise very
impressive project.

--John

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

From: Makarius <makarius@sketis.net>
The "your" cannot mean me, because I am neither responsible for the Java
font-renderer nor for the DejaVu fonts.

I am merely responsible for selecting the best non-legacy technologies
that I could find. If there are even better ones, I will pick them.

Makarius

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

From: Makarius <makarius@sketis.net>
These obersvations are explained in Isabelle2019-RC0/NEWS as follows:

"""

The old Java renderer produced fonts that were too thin, with the
notable exception for 18px. The new one is much better in that respect:
even 12, 14, 16 etc. come out as intended by the DejaVu designers.

Makarius


Last updated: May 01 2024 at 20:18 UTC