src/Pure/Concurrent/par_exn.ML

 evaluations.  Interrupt counts as neutral element.
 *)
 
 signature PAR_EXN =
 sig
-  val serial: exn -> serial * exn
-  val set_serial: exn -> exn
+  val identify: Properties.entry list -> 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
   val release_all: 'a Exn.result list -> 'a list
   val release_first: 'a Exn.result list -> 'a list

 structure Par_Exn: PAR_EXN =
 struct
 
 (* identification via serial numbers *)
 
-fun serial exn =
-  (case get_exn_serial exn of
-    SOME i => (i, exn)
-  | NONE =>
-      let
-        val i = Library.serial ();
-        val exn' = uninterruptible (fn _ => set_exn_serial i) exn;
-      in (i, exn') end);
+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 set_serial exn = #2 (serial exn);
-
-val the_serial = the o get_exn_serial;
+fun the_serial exn =
+  Markup.parse_int (the (Properties.get (Exn_Properties.get exn) Markup.serialN));
 
 val exn_ord = rev_order o int_ord o pairself the_serial;
 
 
 (* parallel exceptions *)

 exception Par_Exn of exn list;
   (*non-empty list with unique identified elements sorted by exn_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 [set_serial exn];
+  | par_exns exn = if Exn.is_interrupt exn then [] else [identify [] exn];
 
 fun make exns =
   (case Ord_List.unions exn_ord (map par_exns exns) of
     [] => Exn.Interrupt
   | es => Par_Exn es);