[isabelle-dev] Option raised errors hides other error failures

Lukas Bulwahn bulwahn at in.tum.de
Fri Sep 9 14:20:11 CEST 2011


Hello all,

lately, I have noticed that the exception handling within the 
non-interactive execution has changed, disguising the true origin of 
exceptions.

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.


Lukas


More information about the isabelle-dev mailing list