[isabelle] Display of exceptions in Isabelle/jEdit



Hallo,

I just noticed the following behaviour of Isabelle/jEdit that Lars Hupel urged me to report:


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
â


Cheers,

Manuel




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