Email Gateway (Aug 22 2022 at 19:27): Email Gateway (Aug 22 2022 at 19:27):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
I tried to download Isabelle2019-RC0 today, but there was some corruption in the tarball.
This comment is based on Isabelle_03-Apr-2019.
I don't normally complain about such things, but yes, the fonts are somewhat blurry.
Beyond that, they are exquisitely ugly, especially the extra wide boldface font
in the Sidekick panel. The appearance in Isabelle 2018 was tolerable, but this new look
is quite bad, IMHO. Besides the boldface keywords being too wide and too bold,
the lines are very crowded and if anything appearing in them has a subscript then
it leads to an ugly variation in line spacing.
Email Gateway (Aug 22 2022 at 19:32):From: Makarius <makarius@sketis.net>
On 05/04/2019 01:38, Eugene W. Stark wrote:
I tried to download Isabelle2019-RC0 today, but there was some corruption in the tarball.
The tarball should be OK -- I have tested it once again. Maybe your
download was corrupted. For comparison, here are
SHA256 checksums and byte sizes
https://isabelle.in.tum.de/website-Isabelle2019-RC0/dist/index.html
This comment is based on Isabelle_03-Apr-2019.
I don't normally complain about such things, but yes, the fonts are somewhat blurry.
That is mainly a function of the font renderer by OpenJDK, but it is
only relevant for very low-resolution displays (HD). The quality is
better than before with non-legacy displays (UHD).
Beyond that, they are exquisitely ugly, especially the extra wide boldface font
in the Sidekick panel.
The new fonts are based on the well-known DejaVu collection. In
particular, there are now a proper Bold / Italic / BoldItalic fonts, not
just interpolations by fontforge or the fontrenderer.
You can check how it is meant to look by the updated Isabelle/jEdit
screenshot:
https://isabelle.in.tum.de/website-Isabelle2019-RC0/img/isabelle_jedit.png
https://isabelle.in.tum.de/website-Isabelle2018/img/isabelle_jedit.png
On my regular UHD display, the 2019 versions looks very good, and the
2018 version looks tolerable, but somewhat bad. On an old HD display
both look bad in different ways.
Makarius
Email Gateway (Aug 22 2022 at 19:33):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
On 4/5/19 9:07 AM, Makarius wrote:
On 05/04/2019 01:38, Eugene W. Stark wrote:
I tried to download Isabelle2019-RC0 today, but there was some corruption in the tarball.
The tarball should be OK -- I have tested it once again. Maybe your
download was corrupted. For comparison, here are
SHA256 checksums and byte sizes
https://isabelle.in.tum.de/website-Isabelle2019-RC0/dist/index.html
Strange. I had gotten the correct number of bytes, but the SHA256 was invalid.
I made another download just now (from home, not in office where I did the other)
and I got a correct SHA256.
This comment is based on Isabelle_03-Apr-2019.
I don't normally complain about such things, but yes, the fonts are somewhat blurry.
That is mainly a function of the font renderer by OpenJDK, but it is
only relevant for very low-resolution displays (HD). The quality is
better than before with non-legacy displays (UHD).
I would not consider the 2560x1440 display I am using to be a very low-resolution
legacy display and the quality is noticeably worse, so indeed relevant.
Beyond that, they are exquisitely ugly, especially the extra wide boldface font
in the Sidekick panel.The new fonts are based on the well-known DejaVu collection. In
particular, there are now a proper Bold / Italic / BoldItalic fonts, not
just interpolations by fontforge or the fontrenderer.You can check how it is meant to look by the updated Isabelle/jEdit
screenshot:https://isabelle.in.tum.de/website-Isabelle2019-RC0/img/isabelle_jedit.png
https://isabelle.in.tum.de/website-Isabelle2018/img/isabelle_jedit.pngOn my regular UHD display, the 2019 versions looks very good, and the
2018 version looks tolerable, but somewhat bad. On an old HD display
both look bad in different ways.
What I see does not show any large differences to the screenshots you posted.
I strongly dislike the boldfaced keywords in the Sidekick panel -- they are
too bold and too wide. The line spacing in that panel is also quite crowded,
IMHO. I prefer the Isabelle 2018 Sidekick to this one by quite a lot.
The line spacing in the main edit panel also appears slightly crowded, to my eye.
I don't know if it is just the difference in the font, or whether the line
spacing was actually reduced. I can tolerate that, but so far I don't like it.
Email Gateway (Aug 22 2022 at 19:33):From: Makarius <makarius@sketis.net>
I was confused about the variation in line spacing, and still am. In
Isabelle2018 I see the same effect.
E.g. use Isabelle Sidekick on the included theory file. Moving with the
mouse over the Sidekick tree makes the bottom status line of the editor
hop up and down. This is a bit ugly, but not a regression.
Maybe it appears to be slightly more ugly now, because the rest of the
GUI looks so great with the new Isabelle DejaVu fonts :-)
Makarius
Scratch.thy
Email Gateway (Aug 22 2022 at 19:33):From: Makarius <makarius@sketis.net>
On 05/04/2019 15:30, Eugene W. Stark wrote:
I would not consider the 2560x1440 display I am using to be a very low-resolution
legacy display and the quality is noticeably worse, so indeed relevant.
I used to have such an Apple Cinema display (30") in my office: that was
very expensive in its time, but is now legacy concerning the resolution.
Of course, if you have that many pixel on 15" it should be fine. (Some
Isabelle user showed me such a laptop a few month ago, and the
Isabelle/jEdit rendering was quite good.)
What I see does not show any large differences to the screenshots you posted.
I strongly dislike the boldfaced keywords in the Sidekick panel -- they are
too bold and too wide. The line spacing in that panel is also quite crowded,
IMHO. I prefer the Isabelle 2018 Sidekick to this one by quite a lot.
Sorry, I cannot follow this. The Sidekick GUI was really bad in
Isabelle2018, especially on macOS. Now it is mostly fine: it looks
better and uses its space better.
The line spacing in the main edit panel also appears slightly crowded, to my eye.
I don't know if it is just the difference in the font, or whether the line
spacing was actually reduced. I can tolerate that, but so far I don't like it.
For the main text area you merely need to adjust
options.textarea.lineSpacing to whatever you prefer: see also "Global
Options / Text Area / Extra vertical line spacing".
The old IsabelleText font was a bit too high, so its default used to be
negative. Now it is at 1px.
Note that it is mainly a matter of getting used to the normal line
height of DejaVu: current displays have less height to waste than in the
past, so I would not deviate too much from its default.
Makarius
Email Gateway (Aug 22 2022 at 19:34):From: Peter Lammich <lammich@in.tum.de>
Hi List,
the font rendering problem on non-highres screens has still not been
fixed.
For me (Ubuntu 16.04) the text display looks considerable worse than
for isabelle2018. The fonts are slightly blurry, which makes serious
working with the IDE really eye-stressing!
I consider this problem actually "release-stopper" critical, as I will
not be able to stare on the display for more than a few minutes without
getting eye problems.
Email Gateway (Aug 22 2022 at 19:35):From: Makarius <makarius@sketis.net>
In the meantime I have made many experiments with old HD displays
(instead of UHD displays that are routinely available since 3 years):
they work fine for me, even after some hours.
Going back to the font rendering of Java 8 is now getting a problem: it
looks strange.
Makarius
Email Gateway (Aug 22 2022 at 19:36):From: Makarius <makarius@sketis.net>
This kind of font rendering has been with OpenJDK for a long time, it is
internally based on FreeType. My impression is that it has recently
improved slighty. Moreover, it seems that the non-free Oracle JDK 11 has
now adopted the same font renderer. So it would not help much to pay
Oracle a per-user fee their commercial Java 11.
The font setup of Isabelle2019-RC0 works reasonably well with my ancient
Sony Vaio 17" HD laptop from 2013 (e.g. 24px for the text area, and Gtk
look-and-feel for the GUI). But that is really historic in many ways.
My current work machine from 2019 is already the second one with UHD
(the first one was from 2014). Now even the on-board Intel graphics has
builtin UHD support at 60 Hz -- older hardware used to have only 30 Hz
(that is not the screen refresh rate, but the frame-buffer update rate,
which is mainly relevant for games).
So why be nostalgic about old hardware? Everyday equipment deserves to
be of good quality, and it is quite cheap, too.
Makarius
Email Gateway (Aug 22 2022 at 19:37):From: Bertram Felgenhauer via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Peter Lammich wrote:
As Makarius wrote, this is a consequence of switching to OpenJDK.
Oracle's JDK uses Bitstream's proprietary T2K font engine, whereas
OpenJDK uses FreeType [1], which as far as I can discern simply does
not support the super-agressive kind of hinting that T2K does on
medium DPI displays.
One can coerce Freetype into doing a bit more. I'm attaching a dirty
LD_PRELOAD hack (sorry, Linux only) that can be used to play with some
options. The most promising one is the 'warping' feature [2], which
attempts to align stems such that one of the sides is pixel aligned.
This avoids the particularly bad case of having two gray pixel columns
next to each other for a vertical stem.
Doing this kind of tweaking properly would require patching the JDK,
unfortunately. See the OpenJDK repo [3] respectively the AdoptOpenJDK
mirror [4].
Cheers,
Bertram
P.S. Speaking for myself I expect I will get used to the new, somewhat
blurrier, look of Isabelle/jEdit on my HD display. The projector
scenario (for teaching) seems to be a more serious concern though.
[1] http://mail.openjdk.java.net/pipermail/discuss/2017-November/004621.html
[2] https://www.freetype.org/freetype2/docs/reference/ft2-properties.html#warping
[3] https://hg.openjdk.java.net/jdk/jdk11/file/tip/src/java.desktop/share/native/libfontmanager/freetypeScaler.c
[4] https://github.com/AdoptOpenJDK/openjdk-jdk11/blob/master/src/java.desktop/share/native/libfontmanager/freetypeScaler.c
grr.c
Email Gateway (Aug 22 2022 at 19:38):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
FWIW I explored some options settings (Utilities>Global Options>jEdit>Text Area),
and I found that, at least in the case of my system/display, the default setting
of "subpixel HRGB" for "Anti Aliased smooth text" produced the worst results of
all of the settings except for "none". I have been using the setting "Standard"
and I think I like it better.
That helps with the main edit window. It doesn't help with the way the fonts
look in pop-up tooltips (they are sort of rough-looking, but I don't look at them
for too long), or the wide boldface that I have already complained about in
the Sidekick panel.
Also, the apparent number of somewhat different faces is disconcerting.
I don't really understand why the search menu has to use a different face in the
text area than the main edit window.
Email Gateway (Aug 22 2022 at 19:38):From: Makarius <makarius@sketis.net>
Yes, I think I will return to "Standard" as default: I've seen odd
effects elsewhere due to "subpixel HRGB".
Makarius
Email Gateway (Aug 22 2022 at 19:39):From: Makarius <makarius@sketis.net>
Thanks indeed. These links shed some true light on this issue.
The mail thread from 2017-November refers to the need for "zero
differences between the OpenJDK and the Oracle JDK". My impression is
that Oracle did this in its commercial Java 11 already: i.e. the font
rendering is now like OpenJDK.
The original JDK sources are also interesting, but I do not have the
ambition to patch that (as I routinely do for the rather small jEdit
codebase).
Makarius
Last updated: Apr 26 2024 at 08:19 UTC