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

[Lukas Bulwahn]

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