--- 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;