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

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:


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