[isabelle-dev] Wrong position information in 3bfa28b3a5b2
makarius at sketis.net
Sun Feb 24 13:15:42 CET 2019
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
>> 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:
date: Sun Feb 24 13:00:43 2019 +0100
files: Admin/components/components.sha1 Admin/components/main
updated to jedit_build-20190224 (new patches: favorites, glyphvector);
date: Sun Feb 24 12:53:23 2019 +0100
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
but jEdit cannot handle that. So I made a fallback to something that is
closer to the old behaviour in Java 8.
More information about the isabelle-dev