[isabelle-dev] Option raised errors hides other error failures
bulwahn at in.tum.de
Fri Sep 9 14:20:11 CEST 2011
lately, I have noticed that the exception handling within the
non-interactive execution has changed, disguising the true origin of
In my concrete case:
When running the compilation within the make command, I get:
*** exception Option raised
Exception- TOPLEVEL_ERROR raised
*** ML error
Whereas running it interactively in PG:
*** exception Match raised
*** At command "code_reflect"
The Match raised is the real reason for the exception in my case, and
the one I was expecting.
The Option raised exception seems to caused somehow as a consequence of
the previous exception within the non-interactive run.
Is this an intended behaviour?
If so, it might be good to know for other developers, not to be mislead
by the error message.
More information about the isabelle-dev