[isabelle-dev] Wrong position information in 3bfa28b3a5b2

Manuel Eberl eberlm at in.tum.de
Fri Feb 22 16:47:01 CET 2019

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". Clicking anywhere after the initial "𝒜" also leads to the
caret being put too far to the left. 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.

In Isabelle 2018, everything works as expected. I do not have the time
to do a bisection right now, but I can do one if it helps.



More information about the isabelle-dev mailing list