Email Gateway (Aug 22 2022 at 12:53): Email Gateway (Aug 22 2022 at 12:53):From: Manuel Eberl <eberlm@in.tum.de>
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
Email Gateway (Aug 22 2022 at 13:07):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 22 2022 at 13:07):From: David Matthews <dm@prolingua.co.uk>
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
Last updated: Apr 26 2024 at 01:06 UTC