Re: [isabelle] Display of exceptions in Isabelle/jEdit



On 09/04/2016 22:46, Makarius wrote:
On Thu, 31 Mar 2016, Manuel Eberl wrote:

In the following example, only the one line that causes the exception
is underlined in red:

ML â
 val _ = raise Div
â


However, in the next example, the entire ML block is marked in red and
it is less clear where the error comes from:

ML â
val x = 1 div 0
â

Isabelle/PIDE merely manages the results produced by Poly/ML.

So this question is actually for David Matthews, who is often reading
isabelle-users, but more often on the Poly/ML mailing list:
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml


     Makarius

It is a question for me but to some extent it depends on how Makarius interprets the results that Poly/ML gives him. What I suspect is happening is that in the first case when an exception is explicitly raised the compiler can insert the location information into the exception packet. In the second case the exception is raised as part of the evaluation of the "div" function. At best it could provide information related to where the "div" function was defined but because "div" is built-in it can't even do that so the location information associated with the Div exception packet is empty.

David




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