On 22/02/2019 22:59, Makarius wrote: > On 22/02/2019 16:47, Manuel Eberl wrote: >> I came upon a regrssion with the position information in terms that >> contain calligraphic or Fraktur letters, e.g.: >> >> theory Scratch >> imports Pure >> begin >> >> lemma "𝒜 𝒜 𝒜 𝒜 ()) a b c d e" >> >> The syntax error in this line is at the second closing parenthesis. In >> 3bfa28b3a5b2, Isabelle/jEdit displays the error at the space between "a" >> and "b". > > This is a problem introduced by Java 11: it works fine with Java 8. (I > will investigate it further later.)
See now the following changes: changeset: 69840:a35033167f01 tag: tip user: wenzelm date: Sun Feb 24 13:00:43 2019 +0100 files: Admin/components/components.sha1 Admin/components/main description: updated to jedit_build-20190224 (new patches: favorites, glyphvector); changeset: 69839:828f3cd0dcf9 user: wenzelm date: Sun Feb 24 12:53:23 2019 +0100 files: src/Tools/jEdit/patches/glyphvector description: fallback on createGlyphVector for multi-character glyphs (e.g. 0x01d49c), as seen in Java 11; Java 11 correctly produces a complex glyph vector layout according to https://docs.oracle.com/en/java/javase/11/docs/api/java.desktop/java/awt/Font.html#layoutGlyphVector(java.awt.font.FontRenderContext,char[],int,int,int) but jEdit cannot handle that. So I made a fallback to something that is closer to the old behaviour in Java 8. Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev