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".
Thanks for keeping an eye on isabelle-dev versions. This is a problem introduced by Java 11: it works fine with Java 8. (I will investigate it further later.) > Each "𝒜" seems to shift the offset > further, so I guess there's an off-by-one error in there somewhere. > Interestingly, not all letters cause this – e.g. "ℳ" seems to be fine. The calligraphic "A" belongs to a different Unicode standard than the calligraphc "M". E.g. see these results in Console / BeanShell or Console / Scala: > "𝒜".length() 2 > "ℳ".length() 1 Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev