Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle2016-1-RC0: error markup too large


view this post on Zulip 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: Mar 29 2024 at 04:18 UTC