[isabelle-dev] [OT] Checked "assume" command

[Lawrence Paulson]

If it is unambiguously wrong, then the highlighting must be as bold as in the case of a syntax error. 
Larry

On 5 Sep 2012, at 14:35, Makarius <makarius at sketis.net> wrote:

> With the "case that must fail" we are getting back to the tendencies of this thread: https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2012-May/002736.html
> where I failed to explain basic observations how warnings and errors get a slightly different meaning in the Prover IDE model.
> 
> Concerning fixes (and implicit type abstractions) you know my basic plan already: highlight the situation in the source text in a way that tells the user what is there, and the user can then see by himself if it is what he had in mind or should have in mind.