While re-engineering ancient code I see that exception handling has
changed in the last years. I see the many (* FIXME avoid handle _ *),
the rules for exception handling within tactics in The Isabelle/Isar
Implementation manual, suggestions for thread-safe handling etc.
Now a simple question, which might be caused by my missing experience of
how to handle Toplevel errors:
I want to adapt code which tries to check types somehow as follows:
ML {*
Toplevel.debug := true;
cterm_of @{theory} (@{term "a"} $ @{term "b"})
handle TYPE _ => writeln "type error found";
*}
This results in the response buffer with:
*** val it = () : unit
*** Error (line 3):
*** Can't unify cterm to {} (Incompatible types)
*** Exception- ERROR "Static Errors" raised
*** At command "ML".
How are such type checks done nowadays ?
Walther
PS: I know that ctxt's are to be preferred to thy's; this will be done
in the next step of re-engineering.
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
