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
