# HG changeset patch
# User wenzelm
# Date 1358331926 -3600
# Node ID b2fb1ab1475dbd30b60e2acfc7575307862fa65c
# Parent  db99fcf697615afb4bb0a542d8d4d623a77ed9fd
tuned signature;

diff -r db99fcf69761 -r b2fb1ab1475d src/Pure/Concurrent/future.ML
--- 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 _ =>
diff -r db99fcf69761 -r b2fb1ab1475d src/Pure/Concurrent/par_exn.ML
--- 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
diff -r db99fcf69761 -r b2fb1ab1475d src/Pure/ML-Systems/polyml.ML
--- 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