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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
