distinguish proper interrupts from Poly/ML RTS breakdown;

--- a/NEWS	Wed Oct 11 14:03:16 2023 +0200
+++ b/NEWS	Thu Oct 12 10:56:45 2023 +0200
@@ -33,6 +33,12 @@
 INCOMPATIBILITY, better use \<^try>\<open>...\<close> with 'catch' or 'finally', or
 as last resort declare [[ML_catch_all]] within the theory context.
 
+* Proper interrupts (e.g. timeouts) are now distinguished from Poly/ML
+runtime system breakdown, using Exn.Interrupt_Breakdown as quasi-error.
+Exn.is_interrupt covers all kinds of interrupts as before, but
+Exn.is_interrupt_proper and Exn.is_interrupt_breakdown are more
+specific. Subtle INCOMPATIBILITY in the semantics of ML evaluation.
+
 
 *** HOL ***
 

--- a/src/Pure/Concurrent/isabelle_thread.ML	Wed Oct 11 14:03:16 2023 +0200
+++ b/src/Pure/Concurrent/isabelle_thread.ML	Thu Oct 12 10:56:45 2023 +0200
@@ -42,7 +42,7 @@
 
 (* abstract type *)
 
-abstype T = T of {thread: Thread.Thread.thread, name: string, id: int}
+abstype T = T of {thread: Thread.Thread.thread, name: string, id: int, break: bool Synchronized.var}
 with
   val make = T;
   fun dest (T args) = args;
@@ -69,7 +69,8 @@
 
 fun init_self name =
   let
-    val t = make {thread = Thread.Thread.self (), name = name, id = make_id ()};
+    val break = Synchronized.var "Isabelle_Thread.break" false;
+    val t = make {thread = Thread.Thread.self (), name = name, id = make_id (), break = break};
   in Thread_Data.put self_var (SOME t); t end;
 
 fun self () =
@@ -136,13 +137,25 @@
 
 (* interrupts *)
 
-val interrupt = Thread.Thread.Interrupt;
+val interrupt = Exn.Interrupt_Break;
 val interrupt_exn = Exn.Exn interrupt;
 
 fun interrupt_self () = raise interrupt;
 
 fun interrupt_other t =
-  Thread.Thread.interrupt (get_thread t) handle Thread.Thread _ => ();
+  Synchronized.change (#break (dest t))
+    (fn b => (Thread.Thread.interrupt (get_thread t); true) handle Thread.Thread _ => b);
+
+fun check_interrupt exn =
+  if Exn.is_interrupt_raw exn then
+    let
+      val t = self ();
+      val break = Synchronized.change_result (#break (dest t)) (fn b => (b, false));
+    in if break then Exn.Interrupt_Break else Exn.Interrupt_Breakdown end
+  else exn;
+
+fun check_interrupt_exn result =
+  Exn.map_exn check_interrupt result;
 
 structure Exn: EXN =
 struct
@@ -157,7 +170,7 @@
     fun main () =
       (Thread_Attributes.set_attributes Thread_Attributes.test_interrupts;
        Thread.Thread.testInterrupt ());
-    val test = Exn.capture_body main;
+    val test = check_interrupt_exn (Exn.capture_body main);
     val _ = Thread_Attributes.set_attributes orig_atts;
   in test end;
 
@@ -165,11 +178,12 @@
 
 fun try_catch e f =
   Thread_Attributes.uninterruptible_body (fn run =>
-    run e () handle exn => if Exn.is_interrupt exn then Exn.reraise exn else f exn);
+    run e () handle exn =>
+      if Exn.is_interrupt exn then Exn.reraise (check_interrupt exn) else f exn);
 
 fun try_finally e f =
   Thread_Attributes.uninterruptible_body (fn run =>
-    Exn.release (Exn.capture_body (run e) before f ()));
+    Exn.release (check_interrupt_exn (Exn.capture_body (run e)) before f ()));
 
 fun try e = Basics.try e ();
 fun can e = Basics.can e ();

--- a/src/Pure/Concurrent/par_exn.ML	Wed Oct 11 14:03:16 2023 +0200
+++ b/src/Pure/Concurrent/par_exn.ML	Thu Oct 12 10:56:45 2023 +0200
@@ -21,10 +21,10 @@
 
 exception Par_Exn of exn list;
   (*non-empty list with unique identified elements sorted by Exn_Properties.ord;
-    no occurrences of Par_Exn or Exn.is_interrupt*)
+    no occurrences of Par_Exn or Exn.is_interrupt_proper*)
 
 fun par_exns (Par_Exn exns) = exns
-  | par_exns exn = if Exn.is_interrupt exn then [] else [Exn_Properties.identify [] exn];
+  | par_exns exn = if Exn.is_interrupt_proper exn then [] else [Exn_Properties.identify [] exn];
 
 fun make exns =
   let
@@ -33,14 +33,14 @@
   in if null exns' then Isabelle_Thread.interrupt else Par_Exn exns' end;
 
 fun dest (Par_Exn exns) = SOME exns
-  | dest exn = if Exn.is_interrupt exn then SOME [] else NONE;
+  | dest exn = if Exn.is_interrupt_proper exn then SOME [] else NONE;
 
 
 (* parallel results *)
 
 fun is_interrupted results =
   exists Exn.is_exn results andalso
-    Exn.is_interrupt (make (map_filter Exn.get_exn results));
+    Exn.is_interrupt_proper (make (map_filter Exn.get_exn results));
 
 fun release_all results =
   if forall Exn.is_res results
@@ -49,7 +49,7 @@
 
 fun plain_exn (Exn.Res _) = NONE
   | plain_exn (Exn.Exn (Par_Exn _)) = NONE
-  | plain_exn (Exn.Exn exn) = if Exn.is_interrupt exn then NONE else SOME exn;
+  | plain_exn (Exn.Exn exn) = if Exn.is_interrupt_proper exn then NONE else SOME exn;
 
 fun release_first results =
   (case get_first plain_exn results of

--- a/src/Pure/General/exn.ML	Wed Oct 11 14:03:16 2023 +0200
+++ b/src/Pure/General/exn.ML	Thu Oct 12 10:56:45 2023 +0200
@@ -27,7 +27,14 @@
   val maps_res: ('a -> 'b result) -> 'a result -> 'b result
   val map_exn: (exn -> exn) -> 'a result -> 'a result
   val cause: exn -> exn
+  exception Interrupt_Break
+  exception Interrupt_Breakdown
+  val is_interrupt_raw: exn -> bool
+  val is_interrupt_break: exn -> bool
+  val is_interrupt_breakdown: exn -> bool
+  val is_interrupt_proper: exn -> bool
   val is_interrupt: exn -> bool
+  val is_interrupt_proper_exn: 'a result -> bool
   val is_interrupt_exn: 'a result -> bool
   val result: ('a -> 'b) -> 'a -> 'b result
   val failure_rc: exn -> int
@@ -100,10 +107,17 @@
 fun cause (IO.Io {cause = exn, ...}) = cause exn
   | cause exn = exn;
 
-fun is_interrupt exn =
-  (case cause exn of
-    Thread.Thread.Interrupt => true
-  | _ => false);
+exception Interrupt_Break;
+exception Interrupt_Breakdown;
+
+fun is_interrupt_raw exn = (case cause exn of Thread.Thread.Interrupt => true | _ => false);
+fun is_interrupt_break exn = (case cause exn of Interrupt_Break => true | _ => false);
+fun is_interrupt_breakdown exn = (case cause exn of Interrupt_Breakdown => true | _ => false);
+fun is_interrupt_proper exn = is_interrupt_raw exn orelse is_interrupt_break exn;
+fun is_interrupt exn = is_interrupt_proper exn orelse is_interrupt_breakdown exn;
+
+fun is_interrupt_proper_exn (Exn exn) = is_interrupt_proper exn
+  | is_interrupt_proper_exn _ = false;
 
 fun is_interrupt_exn (Exn exn) = is_interrupt exn
   | is_interrupt_exn _ = false;

--- a/src/Pure/Isar/toplevel.ML	Wed Oct 11 14:03:16 2023 +0200
+++ b/src/Pure/Isar/toplevel.ML	Thu Oct 12 10:56:45 2023 +0200
@@ -662,7 +662,7 @@
   (case transition int tr st of
     (st', NONE) => st'
   | (_, SOME (exn, info)) =>
-      if Exn.is_interrupt exn then Exn.reraise exn
+      if Exn.is_interrupt_proper exn then Exn.reraise exn
       else raise Runtime.EXCURSION_FAIL (exn, info));
 
 val command = command_exception false;

--- a/src/Pure/ML/exn_properties.ML	Wed Oct 11 14:03:16 2023 +0200
+++ b/src/Pure/ML/exn_properties.ML	Thu Oct 12 10:56:45 2023 +0200
@@ -72,7 +72,7 @@
 (* identification via serial numbers *)
 
 fun identify default_props exn =
-  if Exn.is_interrupt exn then exn
+  if Exn.is_interrupt_proper exn then exn
   else
     let
       val props = get exn;

--- a/src/Pure/proofterm.ML	Wed Oct 11 14:03:16 2023 +0200
+++ b/src/Pure/proofterm.ML	Thu Oct 12 10:56:45 2023 +0200
@@ -2245,9 +2245,8 @@
           (case Exn.capture_body export_body of
             Exn.Res res => res
           | Exn.Exn exn =>
-              if Exn.is_interrupt exn then
-                raise Fail ("Interrupt: potential resource problems while exporting proof " ^
-                  string_of_int i)
+              if Exn.is_interrupt_breakdown exn then
+                raise Fail ("Resource problems while exporting proof " ^ string_of_int i)
               else Exn.reraise exn))
       else no_export;