# HG changeset patch
# User wenzelm
# Date 1695979159 -7200
# Node ID fc0814e9f7a8cce559891f5ba78d0dba0560b581
# Parent  72631efa3821399ba5808f5f9ef3b12036c74a97
more NEWS;

diff -r 72631efa3821 -r fc0814e9f7a8 NEWS
--- a/NEWS	Thu Sep 28 20:07:30 2023 +0200
+++ b/NEWS	Fri Sep 29 11:19:19 2023 +0200
@@ -16,6 +16,19 @@
 
 *** 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>\<open>EXPR catch HANDLER\<close>
+  \<^try>\<open>EXPR finally HANDLER\<close>
+  \<^try>\<open>EXPR\<close>
+
+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>\<open>...\<close> with 'catch' or 'finally', or
 as last resort declare [[ML_catch_all]] within the theory context.