clarified signature: distinction of unmanaged vs. managed interrupts (not implemented yet);

--- a/src/Pure/Concurrent/isabelle_thread.ML	Mon Sep 25 21:58:58 2023 +0200
+++ b/src/Pure/Concurrent/isabelle_thread.ML	Tue Sep 26 12:30:08 2023 +0200
@@ -25,6 +25,7 @@
   val interrupt_exn: 'a Exn.result
   val interrupt_self: unit -> 'a
   val interrupt_other: T -> unit
+  structure Exn: EXN
   val expose_interrupt_result: unit -> unit Exn.result
   val expose_interrupt: unit -> unit  (*exception Interrupt*)
   val try_catch: (unit -> 'a) -> (exn -> 'a) -> 'a
@@ -123,6 +124,12 @@
 fun interrupt_other t =
   Thread.Thread.interrupt (get_thread t) handle Thread.Thread _ => ();
 
+structure Exn: EXN =
+struct
+  open Exn;
+  val capture = capture0;
+end;
+
 fun expose_interrupt_result () =
   let
     val orig_atts = Thread_Attributes.safe_interrupts (Thread_Attributes.get_attributes ());
@@ -146,3 +153,5 @@
 fun can e = Basics.can e ();
 
 end;
+
+structure Exn = Isabelle_Thread.Exn;

--- a/src/Pure/Concurrent/multithreading.ML	Mon Sep 25 21:58:58 2023 +0200
+++ b/src/Pure/Concurrent/multithreading.ML	Tue Sep 26 12:30:08 2023 +0200
@@ -96,14 +96,14 @@
               val time = Timer.checkRealTimer timer;
               val _ = tracing_time true time (fn () => name ^ ": locked after " ^ Time.toString time);
             in false end;
-        val result = Exn.capture (restore_attributes e) ();
+        val result = Exn.capture0 (restore_attributes e) ();
         val _ = if immediate then () else tracing 5 (fn () => name ^ ": unlocking ...");
         val _ = Thread.Mutex.unlock lock;
       in result end
     else
       let
         val _ = Thread.Mutex.lock lock;
-        val result = Exn.capture (restore_attributes e) ();
+        val result = Exn.capture0 (restore_attributes e) ();
         val _ = Thread.Mutex.unlock lock;
       in result end) ());
 

--- a/src/Pure/Concurrent/thread_attributes.ML	Mon Sep 25 21:58:58 2023 +0200
+++ b/src/Pure/Concurrent/thread_attributes.ML	Tue Sep 26 12:30:08 2023 +0200
@@ -95,7 +95,7 @@
     if atts1 = atts2 then e atts1
     else
       let
-        val result = Exn.capture (fn () => (set_attributes atts2; e atts1)) ();
+        val result = Exn.capture0 (fn () => (set_attributes atts2; e atts1)) ();
         val _ = set_attributes atts1;
       in Exn.release result end
   end;

--- a/src/Pure/Concurrent/thread_data.ML	Mon Sep 25 21:58:58 2023 +0200
+++ b/src/Pure/Concurrent/thread_data.ML	Tue Sep 26 12:30:08 2023 +0200
@@ -34,7 +34,7 @@
     let
       val orig_data = get v;
       val _ = put v data;
-      val result = Exn.capture (restore_attributes f) x;
+      val result = Exn.capture0 (restore_attributes f) x;
       val _ = put v orig_data;
     in Exn.release result end) ();
 

--- a/src/Pure/Concurrent/unsynchronized.ML	Mon Sep 25 21:58:58 2023 +0200
+++ b/src/Pure/Concurrent/unsynchronized.ML	Tue Sep 26 12:30:08 2023 +0200
@@ -43,7 +43,7 @@
     let
       val orig_value = ! flag;
       val _ = flag := value;
-      val result = Exn.capture (restore_attributes f) x;
+      val result = Exn.capture0 (restore_attributes f) x;
       val _ = flag := orig_value;
     in Exn.release result end) ();
 

--- a/src/Pure/General/exn.ML	Mon Sep 25 21:58:58 2023 +0200
+++ b/src/Pure/General/exn.ML	Tue Sep 26 12:30:08 2023 +0200
@@ -11,7 +11,7 @@
   val cat_error: string -> string -> 'a
 end;
 
-signature EXN =
+signature EXN0 =
 sig
   include BASIC_EXN
   val polyml_location: exn -> PolyML.location option
@@ -21,7 +21,7 @@
   val is_exn: 'a result -> bool
   val get_res: 'a result -> 'a option
   val get_exn: 'a result -> exn option
-  val capture: ('a -> 'b) -> 'a -> 'b result
+  val capture0: ('a -> 'b) -> 'a -> 'b result  (*unmanaged interrupts*)
   val release: 'a result -> 'a
   val map_res: ('a -> 'b) -> 'a result -> 'b result
   val maps_res: ('a -> 'b result) -> 'a result -> 'b result
@@ -35,7 +35,13 @@
   val trace: (exn -> string) -> (string -> unit) -> (unit -> 'a) -> 'a
 end;
 
-structure Exn: EXN =
+signature EXN =
+sig
+  include EXN0
+  val capture: ('a -> 'b) -> 'a -> 'b result  (*managed interrupts*)
+end;
+
+structure Exn: EXN0 =
 struct
 
 (* location *)
@@ -74,7 +80,7 @@
 fun get_exn (Exn exn) = SOME exn
   | get_exn _ = NONE;
 
-fun capture f x = Res (f x) handle e => Exn e;
+fun capture0 f x = Res (f x) handle e => Exn e;
 
 fun release (Res y) = y
   | release (Exn e) = reraise e;