--- a/src/Pure/Concurrent/par_exn.ML Thu Sep 21 17:09:48 2023 +0200
+++ b/src/Pure/Concurrent/par_exn.ML Thu Sep 21 18:14:28 2023 +0200
@@ -7,8 +7,6 @@
signature PAR_EXN =
sig
- val identify: Properties.T -> exn -> exn
- val the_serial: exn -> int
val make: exn list -> exn
val dest: exn -> exn list option
val is_interrupted: 'a Exn.result list -> bool
@@ -19,36 +17,19 @@
structure Par_Exn: PAR_EXN =
struct
-(* identification via serial numbers -- NOT portable! *)
-
-fun identify default_props exn =
- let
- val props = Exn_Properties.get exn;
- val update_serial =
- if Properties.defined props Markup.serialN then []
- else [(Markup.serialN, serial_string ())];
- val update_props = filter_out (Properties.defined props o #1) default_props;
- in Exn_Properties.update (update_serial @ update_props) exn end;
-
-fun the_serial exn =
- Value.parse_int (the (Properties.get (Exn_Properties.get exn) Markup.serialN));
-
-val exn_ord = rev_order o int_ord o apply2 the_serial;
-
-
(* parallel exceptions *)
exception Par_Exn of exn list;
- (*non-empty list with unique identified elements sorted by exn_ord;
+ (*non-empty list with unique identified elements sorted by Exn_Properties.ord;
no occurrences of Par_Exn or Exn.Interrupt*)
fun par_exns (Par_Exn exns) = exns
- | par_exns exn = if Exn.is_interrupt exn then [] else [identify [] exn];
+ | par_exns exn = if Exn.is_interrupt exn then [] else [Exn_Properties.identify [] exn];
fun make exns =
let
val exnss = map par_exns exns;
- val exns' = Ord_List.unions exn_ord exnss handle Option.Option => flat exnss;
+ val exns' = Ord_List.unions Exn_Properties.ord exnss handle Option.Option => flat exnss;
in if null exns' then Exn.Interrupt else Par_Exn exns' end;
fun dest (Par_Exn exns) = SOME exns