Re: [isabelle] jEdit: Limited Unicode Support

On Fri, 29 Jun 2012, Tjark Weber wrote:

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?

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.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.