[isabelle-dev] NEWS: Robust handling of program exceptions in Isabelle/ML

[Makarius]

*** ML ***

* ML antiquotation "try" provides variants of exception handling that
avoids accidental capture of physical interrupts (which could affect ML
semantics in unpredictable ways):

   \<^try>‹EXPR catch HANDLER›
   \<^try>‹EXPR finally HANDLER›
   \<^try>‹EXPR›

See also the implementations Isabelle_Thread.try_catch / try_finally /
try. The HANDLER always runs as uninterruptible, but the EXPR uses the
the current thread attributes (normally interruptible). Various examples
occur in the Isabelle sources (.ML and .thy files).

* Isabelle/ML explicitly rejects 'handle' with catch-all patterns.
INCOMPATIBILITY, better use \<^try>‹...› with 'catch' or 'finally', or
as last resort declare [[ML_catch_all]] within the theory context.


This refers to Isabelle/fc0814e9f7a8 and AFP/9c5fe84ef108.

Instead of friendly hints in the "implementation" manual (which still needs to 
be updated), there are now hard checks in the Isabelle/ML compiler setup and 
proper antiquotations to get things right by construction.

This is only the first stage of a substantial reform in exception handling. 
The next stage will be distinct Exn.Interrupt_Break (interactive thread 
signal) vs. Exn.Interrupt_Breakdown (resource problem in the ML runtime-system).


	Makarius