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: http://lists.inf.ed.ac.uk/mailman/listinfo/polyml


	Makarius


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