Email Gateway (Aug 22 2022 at 14:23): Email Gateway (Aug 22 2022 at 14:23):From: Makarius <makarius@sketis.net>
The question here is what exactly is the range of a command span. When
there is no specific position for messages, sometimes the whole span is
used, sometimes only the main command keyword.
The details have change back and forth several times, but the situation
has been mostly stable for some years, at a local minimum for the
potential of user confusion.
Note that this did not change in Isabelle2016-1-RC0. It should be the
same as Isabelle2016, Isabelle2015, Isabelle2014, ...
Makarius
Last updated: Nov 21 2024 at 12:39 UTC