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



On 13/10/16 15:16, Lars Hupel wrote:
> lemma True
> proof -
>   have False
>     sorry
> 
>   ââabcâ

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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.