# HG changeset patch
# User wenzelm
# Date 1695312868 -7200
# Node ID dc7455787a8eac9db4de3e82d3c7baf24e401410
# Parent  5b2391321bab512e4e991a99826385880ac7f691
clarified modules;

diff -r 5b2391321bab -r dc7455787a8e src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Thu Sep 21 17:09:48 2023 +0200
+++ b/src/Pure/Concurrent/future.ML	Thu Sep 21 18:14:28 2023 +0200
@@ -419,7 +419,7 @@
       (case Position.id_of pos of
         NONE => []
       | SOME id => [(Markup.exec_idN, id)])
-    in Par_Exn.identify exec_id exn end);
+    in Exn_Properties.identify exec_id exn end);
 
 fun assign_result group result res =
   let
diff -r 5b2391321bab -r dc7455787a8e src/Pure/Concurrent/par_exn.ML
--- 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
diff -r 5b2391321bab -r dc7455787a8e src/Pure/Isar/runtime.ML
--- a/src/Pure/Isar/runtime.ML	Thu Sep 21 17:09:48 2023 +0200
+++ b/src/Pure/Isar/runtime.ML	Thu Sep 21 18:14:28 2023 +0200
@@ -75,9 +75,9 @@
 
 fun identify exn =
   let
-    val exn' = Par_Exn.identify [] exn;
+    val exn' = Exn_Properties.identify [] exn;
     val exec_id = Properties.get (Exn_Properties.get exn') Markup.exec_idN;
-    val i = Par_Exn.the_serial exn' handle Option.Option => serial ();
+    val i = Exn_Properties.the_serial exn' handle Option.Option => serial ();
   in ((i, exn'), exec_id) end;
 
 fun flatten _ (CONTEXT (ctxt, exn)) = flatten (SOME ctxt) exn
diff -r 5b2391321bab -r dc7455787a8e src/Pure/ML/exn_properties.ML
--- a/src/Pure/ML/exn_properties.ML	Thu Sep 21 17:09:48 2023 +0200
+++ b/src/Pure/ML/exn_properties.ML	Thu Sep 21 18:14:28 2023 +0200
@@ -9,7 +9,9 @@
   val position_of_polyml_location: ML_Compiler0.polyml_location -> Position.T
   val position: exn -> Position.T
   val get: exn -> Properties.T
-  val update: Properties.T -> exn -> exn
+  val identify: Properties.T -> exn -> exn
+  val the_serial: exn -> int
+  val ord: exn ord
 end;
 
 structure Exn_Properties: EXN_PROPERTIES =
@@ -68,4 +70,21 @@
         end
     end;
 
+
+(* identification via serial numbers *)
+
+fun identify default_props exn =
+  let
+    val props = 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 update (update_serial @ update_props) exn end;
+
+fun the_serial exn =
+  Value.parse_int (the (Properties.get (get exn) Markup.serialN));
+
+val ord = rev_order o int_ord o apply2 the_serial;
+
 end;