--- a/src/Pure/Concurrent/future.ML Tue Jan 15 20:51:30 2013 +0100
+++ b/src/Pure/Concurrent/future.ML Wed Jan 16 11:25:26 2013 +0100
@@ -439,7 +439,7 @@
let
val res =
(case raw_res of
- Exn.Exn exn => Exn.Exn (#2 (Par_Exn.serial exn))
+ Exn.Exn exn => Exn.Exn (Par_Exn.set_serial exn)
| _ => raw_res);
val _ = Single_Assignment.assign result res
handle exn as Fail _ =>
--- a/src/Pure/Concurrent/par_exn.ML Tue Jan 15 20:51:30 2013 +0100
+++ b/src/Pure/Concurrent/par_exn.ML Wed Jan 16 11:25:26 2013 +0100
@@ -8,6 +8,7 @@
signature PAR_EXN =
sig
val serial: exn -> serial * exn
+ val set_serial: exn -> exn
val make: exn list -> exn
val dest: exn -> exn list option
val is_interrupted: 'a Exn.result list -> bool
@@ -29,6 +30,8 @@
val exn' = uninterruptible (fn _ => set_exn_serial i) exn;
in (i, exn') end);
+fun set_serial exn = #2 (serial exn);
+
val the_serial = the o get_exn_serial;
val exn_ord = rev_order o int_ord o pairself the_serial;
@@ -41,7 +44,7 @@
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 [#2 (serial exn)];
+ | par_exns exn = if Exn.is_interrupt exn then [] else [set_serial exn];
fun make exns =
(case Ord_List.unions exn_ord (map par_exns exns) of
--- a/src/Pure/ML-Systems/polyml.ML Tue Jan 15 20:51:30 2013 +0100
+++ b/src/Pure/ML-Systems/polyml.ML Wed Jan 16 11:25:26 2013 +0100
@@ -11,7 +11,7 @@
NONE => raise exn
| SOME location => PolyML.raiseWithLocation (exn, location));
-fun set_exn_serial i exn =
+fun set_exn_serial i exn = (*requires uninterruptible*)
let
val (file, startLine, endLine) =
(case PolyML.exceptionLocation exn of