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 <[email protected]> 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. _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
