[isabelle-dev] Error highlighting in ML for @{lemma}

[Makarius]

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