On Sat, 28 Jun 2014, Lars Noschinski wrote:
If I insert a lemma antiquotation in ML code with a proposition with a
type error, the error message is not attached to the proposition or the
antiquotation but to the whole block or file of ML. This refers to
13b06c6261.
That is a consequence of the syntax "check" phases still being without
detailed position information. As a fall-back the position of the command
transaction is used, i.e. the keyword. For 'ML' or 'text' that might be
far away from the occurrence of the error in the antiquotation.
Even more annoying in practice is the lack of positions for type errors in
plain terms within formal specifications of the theory.
I take this report as a reminder and refreshment of the priority of this
non-PIDE compliant part of the system, but it won't be addressed for the
coming release.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
