1.1 --- a/src/Pure/Concurrent/future.ML	Wed Aug 17 22:25:00 2011 +0200
     1.2 +++ b/src/Pure/Concurrent/future.ML	Wed Aug 17 23:37:23 2011 +0200
     1.3 @@ -394,8 +394,12 @@
     1.4  
     1.5  (* future jobs *)
     1.6  
     1.7 -fun assign_result group result res =
     1.8 +fun assign_result group result raw_res =
     1.9    let
    1.10 +    val res =
    1.11 +      (case raw_res of
    1.12 +        Exn.Exn exn => Exn.Exn (#2 (Par_Exn.serial exn))
    1.13 +      | _ => raw_res);
    1.14      val _ = Single_Assignment.assign result res
    1.15        handle exn as Fail _ =>
    1.16          (case Single_Assignment.peek result of

     2.1 --- a/src/Pure/Concurrent/par_exn.ML	Wed Aug 17 22:25:00 2011 +0200
     2.2 +++ b/src/Pure/Concurrent/par_exn.ML	Wed Aug 17 23:37:23 2011 +0200
     2.3 @@ -7,8 +7,9 @@
     2.4  
     2.5  signature PAR_EXN =
     2.6  sig
     2.7 +  val serial: exn -> serial * exn
     2.8    val make: exn list -> exn
     2.9 -  val dest: exn -> (serial * exn) list option
    2.10 +  val dest: exn -> exn list option
    2.11    val release_all: 'a Exn.result list -> 'a list
    2.12    val release_first: 'a Exn.result list -> 'a list
    2.13  end;
    2.14 @@ -16,14 +17,22 @@
    2.15  structure Par_Exn =
    2.16  struct
    2.17  
    2.18 +(* identification via serial numbers *)
    2.19 +
    2.20 +fun serial exn =
    2.21 +  (case get_exn_serial exn of
    2.22 +    SOME i => (i, exn)
    2.23 +  | NONE => let val i = Library.serial () in (i, set_exn_serial i exn) end);
    2.24 +
    2.25 +val exn_ord = rev_order o int_ord o pairself (the o get_exn_serial);
    2.26 +
    2.27 +
    2.28  (* parallel exceptions *)
    2.29  
    2.30 -exception Par_Exn of (serial * exn) Ord_List.T;
    2.31 -
    2.32 -fun exn_ord ((i, _), (j, _)) = int_ord (j, i);
    2.33 +exception Par_Exn of exn Ord_List.T;
    2.34  
    2.35  fun par_exns (Par_Exn exns) = SOME exns
    2.36 -  | par_exns exn = if Exn.is_interrupt exn then NONE else SOME [(serial (), exn)];
    2.37 +  | par_exns exn = if Exn.is_interrupt exn then NONE else SOME [#2 (serial exn)];
    2.38  
    2.39  fun make exns =
    2.40    (case map_filter par_exns exns of

     3.1 --- a/src/Pure/Isar/runtime.ML	Wed Aug 17 22:25:00 2011 +0200
     3.2 +++ b/src/Pure/Isar/runtime.ML	Wed Aug 17 23:37:23 2011 +0200
     3.3 @@ -61,7 +61,7 @@
     3.4        if Exn.is_interrupt exn then []
     3.5        else
     3.6          (case Par_Exn.dest exn of
     3.7 -          SOME exns => maps (exn_msgs context o #2) exns   (* FIXME include serial in message!? *)
     3.8 +          SOME exns => maps (exn_msgs context) exns
     3.9          | NONE =>
    3.10              (case exn of
    3.11                Exn.EXCEPTIONS exns => maps (exn_msgs context) exns

     4.1 --- a/src/Pure/ML-Systems/polyml-5.2.1.ML	Wed Aug 17 22:25:00 2011 +0200
     4.2 +++ b/src/Pure/ML-Systems/polyml-5.2.1.ML	Wed Aug 17 23:37:23 2011 +0200
     4.3 @@ -13,6 +13,8 @@
     4.4  end;
     4.5  
     4.6  fun reraise exn = raise exn;
     4.7 +fun set_exn_serial (_: int) (exn: exn) = exn;
     4.8 +fun get_exn_serial (exn: exn) : int option = NONE;
     4.9  
    4.10  use "ML-Systems/polyml_common.ML";
    4.11  use "ML-Systems/multithreading_polyml.ML";

     5.1 --- a/src/Pure/ML-Systems/polyml.ML	Wed Aug 17 22:25:00 2011 +0200
     5.2 +++ b/src/Pure/ML-Systems/polyml.ML	Wed Aug 17 23:37:23 2011 +0200
     5.3 @@ -17,6 +17,22 @@
     5.4      NONE => raise exn
     5.5    | SOME location => PolyML.raiseWithLocation (exn, location));
     5.6  
     5.7 +fun set_exn_serial i exn =
     5.8 +  let
     5.9 +    val (file, startLine, endLine) =
    5.10 +      (case PolyML.exceptionLocation exn of
    5.11 +        NONE => ("", 0, 0)
    5.12 +      | SOME {file, startLine, endLine, startPosition, ...} => (file, startLine, endLine));
    5.13 +    val location =
    5.14 +      {file = file, startLine = startLine, endLine = endLine,
    5.15 +        startPosition = ~ i, endPosition = 0};
    5.16 +  in PolyML.raiseWithLocation (exn, location) handle e => e end;
    5.17 +
    5.18 +fun get_exn_serial exn =
    5.19 +  (case Option.map #startPosition (PolyML.exceptionLocation exn) of
    5.20 +    NONE => NONE
    5.21 +  | SOME i => if i >= 0 then NONE else SOME (~ i));
    5.22 +
    5.23  use "ML-Systems/polyml_common.ML";
    5.24  use "ML-Systems/multithreading_polyml.ML";
    5.25  use "ML-Systems/unsynchronized.ML";

     6.1 --- a/src/Pure/ML-Systems/smlnj.ML	Wed Aug 17 22:25:00 2011 +0200
     6.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Wed Aug 17 23:37:23 2011 +0200
     6.3 @@ -3,10 +3,13 @@
     6.4  Compatibility file for Standard ML of New Jersey 110 or later.
     6.5  *)
     6.6  
     6.7 +use "ML-Systems/proper_int.ML";
     6.8 +
     6.9  exception Interrupt;
    6.10  fun reraise exn = raise exn;
    6.11 +fun set_exn_serial (_: int) (exn: exn) = exn;
    6.12 +fun get_exn_serial (exn: exn) : int option = NONE;
    6.13  
    6.14 -use "ML-Systems/proper_int.ML";
    6.15  use "ML-Systems/overloading_smlnj.ML";
    6.16  use "General/exn.ML";
    6.17  use "ML-Systems/single_assignment.ML";