Email Gateway (Aug 18 2022 at 20:19): Email Gateway (Aug 18 2022 at 20:19):From: Tjark Weber <webertj@in.tum.de>
Hi,
I just noticed that Isabelle/jEdit (on Linux) does not support the same
Unicode characters as ProofGeneral: when opening src/HOL/ex/Chinese.thy
in Isabelle/jEdit, I see lots of black squares. In ProofGeneral 4.1/
Emacs 23.3.1, I see proper Chinese characters.
Is this a (possibly well-known) current limitation of Isabelle/jEdit,
or a problem with my local configuration?
Best regards,
Tjark
Email Gateway (Aug 18 2022 at 20:19):From: Makarius <makarius@sketis.net>
Yes, these things are all too well-known. I am struggling with Unicode
for several years already. What you see in Isabelle/Scala/jEdit of
Isabelle2012 works in almost all practical situations, so that one could
get the idea that everything should just work, but there are boundary
cases where it doesn't.
Unicode on the JVM is particularly delicate. On Mac OS, the JVM 1.6 by
Apple would collect glyphs from other fonts on the system on demand, in
the same way Firefox would do for example (but this can also lead to
surprises). So here the Chinese.thy would look basically OK, potentially
with slightly odd font-metrics for the Chinise glyphs.
On Linux and Windows, the official JVM by Oracle does nothing like that.
It just renders the Unicode points that are available in the (single) font
that you give to the jEdit text area.
Isabelle/Scala relies on the IsabelleText font, which is my own collection
of many glyphs, including many for Eastern Europe and the Middle East, but
not the Far East (which I cannot read myself, so I did not dare to play
with that).
More recent versions of jEdit provide another user-space glyph replacement
facility for the text area (not the rest of the editor GUI elements), but
I did not try it out yet. It will probably interfere with my text painter
plugin for jEdit, which is required for sub/superscripts with in the text
buffer.
Makarius
Last updated: May 06 2024 at 20:16 UTC