tuned signature;
authorwenzelm
Wed, 16 Jan 2013 11:25:26 +0100
changeset 50909 b2fb1ab1475d
parent 50905 db99fcf69761
child 50910 54f06ba192ef
tuned signature;
src/Pure/Concurrent/future.ML
src/Pure/Concurrent/par_exn.ML
src/Pure/ML-Systems/polyml.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 _ =>
--- 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