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:


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.


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