# HG changeset patch
# User wenzelm
# Date 1313617043 -7200
# Node ID 64620f1d6f879bb493f0ace5d30a5d485a812105
# Parent  6a3541412b23bb0742fb6e8dca5f3c5c573d580a
identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;

diff -r 6a3541412b23 -r 64620f1d6f87 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Wed Aug 17 22:25:00 2011 +0200
+++ b/src/Pure/Concurrent/future.ML	Wed Aug 17 23:37:23 2011 +0200
@@ -394,8 +394,12 @@
 
 (* future jobs *)
 
-fun assign_result group result res =
+fun assign_result group result raw_res =
   let
+    val res =
+      (case raw_res of
+        Exn.Exn exn => Exn.Exn (#2 (Par_Exn.serial exn))
+      | _ => raw_res);
     val _ = Single_Assignment.assign result res
       handle exn as Fail _ =>
         (case Single_Assignment.peek result of
diff -r 6a3541412b23 -r 64620f1d6f87 src/Pure/Concurrent/par_exn.ML
--- a/src/Pure/Concurrent/par_exn.ML	Wed Aug 17 22:25:00 2011 +0200
+++ b/src/Pure/Concurrent/par_exn.ML	Wed Aug 17 23:37:23 2011 +0200
@@ -7,8 +7,9 @@
 
 signature PAR_EXN =
 sig
+  val serial: exn -> serial * exn
   val make: exn list -> exn
-  val dest: exn -> (serial * exn) list option
+  val dest: exn -> exn list option
   val release_all: 'a Exn.result list -> 'a list
   val release_first: 'a Exn.result list -> 'a list
 end;
@@ -16,14 +17,22 @@
 structure 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 () in (i, set_exn_serial i exn) end);
+
+val exn_ord = rev_order o int_ord o pairself (the o get_exn_serial);
+
+
 (* parallel exceptions *)
 
-exception Par_Exn of (serial * exn) Ord_List.T;
-
-fun exn_ord ((i, _), (j, _)) = int_ord (j, i);
+exception Par_Exn of exn Ord_List.T;
 
 fun par_exns (Par_Exn exns) = SOME exns
-  | par_exns exn = if Exn.is_interrupt exn then NONE else SOME [(serial (), exn)];
+  | par_exns exn = if Exn.is_interrupt exn then NONE else SOME [#2 (serial exn)];
 
 fun make exns =
   (case map_filter par_exns exns of
diff -r 6a3541412b23 -r 64620f1d6f87 src/Pure/Isar/runtime.ML
--- a/src/Pure/Isar/runtime.ML	Wed Aug 17 22:25:00 2011 +0200
+++ b/src/Pure/Isar/runtime.ML	Wed Aug 17 23:37:23 2011 +0200
@@ -61,7 +61,7 @@
       if Exn.is_interrupt exn then []
       else
         (case Par_Exn.dest exn of
-          SOME exns => maps (exn_msgs context o #2) exns   (* FIXME include serial in message!? *)
+          SOME exns => maps (exn_msgs context) exns
         | NONE =>
             (case exn of
               Exn.EXCEPTIONS exns => maps (exn_msgs context) exns
diff -r 6a3541412b23 -r 64620f1d6f87 src/Pure/ML-Systems/polyml-5.2.1.ML
--- a/src/Pure/ML-Systems/polyml-5.2.1.ML	Wed Aug 17 22:25:00 2011 +0200
+++ b/src/Pure/ML-Systems/polyml-5.2.1.ML	Wed Aug 17 23:37:23 2011 +0200
@@ -13,6 +13,8 @@
 end;
 
 fun reraise exn = raise exn;
+fun set_exn_serial (_: int) (exn: exn) = exn;
+fun get_exn_serial (exn: exn) : int option = NONE;
 
 use "ML-Systems/polyml_common.ML";
 use "ML-Systems/multithreading_polyml.ML";
diff -r 6a3541412b23 -r 64620f1d6f87 src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Wed Aug 17 22:25:00 2011 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Wed Aug 17 23:37:23 2011 +0200
@@ -17,6 +17,22 @@
     NONE => raise exn
   | SOME location => PolyML.raiseWithLocation (exn, location));
 
+fun set_exn_serial i exn =
+  let
+    val (file, startLine, endLine) =
+      (case PolyML.exceptionLocation exn of
+        NONE => ("", 0, 0)
+      | SOME {file, startLine, endLine, startPosition, ...} => (file, startLine, endLine));
+    val location =
+      {file = file, startLine = startLine, endLine = endLine,
+        startPosition = ~ i, endPosition = 0};
+  in PolyML.raiseWithLocation (exn, location) handle e => e end;
+
+fun get_exn_serial exn =
+  (case Option.map #startPosition (PolyML.exceptionLocation exn) of
+    NONE => NONE
+  | SOME i => if i >= 0 then NONE else SOME (~ i));
+
 use "ML-Systems/polyml_common.ML";
 use "ML-Systems/multithreading_polyml.ML";
 use "ML-Systems/unsynchronized.ML";
diff -r 6a3541412b23 -r 64620f1d6f87 src/Pure/ML-Systems/smlnj.ML
--- a/src/Pure/ML-Systems/smlnj.ML	Wed Aug 17 22:25:00 2011 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML	Wed Aug 17 23:37:23 2011 +0200
@@ -3,10 +3,13 @@
 Compatibility file for Standard ML of New Jersey 110 or later.
 *)
 
+use "ML-Systems/proper_int.ML";
+
 exception Interrupt;
 fun reraise exn = raise exn;
+fun set_exn_serial (_: int) (exn: exn) = exn;
+fun get_exn_serial (exn: exn) : int option = NONE;
 
-use "ML-Systems/proper_int.ML";
 use "ML-Systems/overloading_smlnj.ML";
 use "General/exn.ML";
 use "ML-Systems/single_assignment.ML";