merged
authorhuffman
Wed Aug 17 15:12:34 2011 -0700 (2011-08-17)
changeset 44262355d5438f5fb
parent 44261 e44f465c00a1
parent 44258 a93426812ad5
child 44263 971d1be5d5ce
merged
     1.1 --- a/Admin/polyml/future/ROOT.ML	Wed Aug 17 15:03:30 2011 -0700
     1.2 +++ b/Admin/polyml/future/ROOT.ML	Wed Aug 17 15:12:34 2011 -0700
     1.3 @@ -7,6 +7,22 @@
     1.4      NONE => raise exn
     1.5    | SOME location => PolyML.raiseWithLocation (exn, location));
     1.6  
     1.7 +fun set_exn_serial i exn =
     1.8 +  let
     1.9 +    val (file, startLine, endLine) =
    1.10 +      (case PolyML.exceptionLocation exn of
    1.11 +        NONE => ("", 0, 0)
    1.12 +      | SOME {file, startLine, endLine, startPosition, ...} => (file, startLine, endLine));
    1.13 +    val location =
    1.14 +      {file = file, startLine = startLine, endLine = endLine,
    1.15 +        startPosition = ~ i, endPosition = 0};
    1.16 +  in PolyML.raiseWithLocation (exn, location) handle e => e end;
    1.17 +
    1.18 +fun get_exn_serial exn =
    1.19 +  (case Option.map #startPosition (PolyML.exceptionLocation exn) of
    1.20 +    NONE => NONE
    1.21 +  | SOME i => if i >= 0 then NONE else SOME (~ i));
    1.22 +
    1.23  exception Interrupt = SML90.Interrupt;
    1.24  val ord = SML90.ord;
    1.25  val chr = SML90.chr;
    1.26 @@ -61,6 +77,7 @@
    1.27  use "General/alist.ML";
    1.28  use "General/table.ML";
    1.29  use "General/graph.ML";
    1.30 +use "General/ord_list.ML";
    1.31  
    1.32  structure Position =
    1.33  struct
    1.34 @@ -89,6 +106,7 @@
    1.35  use "General/markup.ML";
    1.36  use "Concurrent/single_assignment.ML";
    1.37  use "Concurrent/time_limit.ML";
    1.38 +use "Concurrent/par_exn.ML";
    1.39  use "Concurrent/task_queue.ML";
    1.40  use "Concurrent/future.ML";
    1.41  use "Concurrent/lazy.ML";
     2.1 --- a/src/Pure/Concurrent/future.ML	Wed Aug 17 15:03:30 2011 -0700
     2.2 +++ b/src/Pure/Concurrent/future.ML	Wed Aug 17 15:12:34 2011 -0700
     2.3 @@ -394,8 +394,12 @@
     2.4  
     2.5  (* future jobs *)
     2.6  
     2.7 -fun assign_result group result res =
     2.8 +fun assign_result group result raw_res =
     2.9    let
    2.10 +    val res =
    2.11 +      (case raw_res of
    2.12 +        Exn.Exn exn => Exn.Exn (#2 (Par_Exn.serial exn))
    2.13 +      | _ => raw_res);
    2.14      val _ = Single_Assignment.assign result res
    2.15        handle exn as Fail _ =>
    2.16          (case Single_Assignment.peek result of
    2.17 @@ -473,9 +477,9 @@
    2.18      NONE => Exn.Exn (Fail "Unfinished future")
    2.19    | SOME res =>
    2.20        if Exn.is_interrupt_exn res then
    2.21 -        (case Exn.flatten_list (Task_Queue.group_status (Task_Queue.group_of_task (task_of x))) of
    2.22 -          [] => res
    2.23 -        | exns => Exn.Exn (Exn.EXCEPTIONS exns))
    2.24 +        (case Task_Queue.group_status (Task_Queue.group_of_task (task_of x)) of
    2.25 +          NONE => res
    2.26 +        | SOME exn => Exn.Exn exn)
    2.27        else res);
    2.28  
    2.29  fun join_next deps = (*requires SYNCHRONIZED*)
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/Concurrent/par_exn.ML	Wed Aug 17 15:12:34 2011 -0700
     3.3 @@ -0,0 +1,63 @@
     3.4 +(*  Title:      Pure/Concurrent/par_exn.ML
     3.5 +    Author:     Makarius
     3.6 +
     3.7 +Parallel exceptions as flattened results from acyclic graph of
     3.8 +evaluations.  Interrupt counts as neutral element.
     3.9 +*)
    3.10 +
    3.11 +signature PAR_EXN =
    3.12 +sig
    3.13 +  val serial: exn -> serial * exn
    3.14 +  val make: exn list -> exn
    3.15 +  val dest: exn -> exn list option
    3.16 +  val release_all: 'a Exn.result list -> 'a list
    3.17 +  val release_first: 'a Exn.result list -> 'a list
    3.18 +end;
    3.19 +
    3.20 +structure Par_Exn =
    3.21 +struct
    3.22 +
    3.23 +(* identification via serial numbers *)
    3.24 +
    3.25 +fun serial exn =
    3.26 +  (case get_exn_serial exn of
    3.27 +    SOME i => (i, exn)
    3.28 +  | NONE => let val i = Library.serial () in (i, set_exn_serial i exn) end);
    3.29 +
    3.30 +val exn_ord = rev_order o int_ord o pairself (the o get_exn_serial);
    3.31 +
    3.32 +
    3.33 +(* parallel exceptions *)
    3.34 +
    3.35 +exception Par_Exn of exn Ord_List.T;
    3.36 +
    3.37 +fun par_exns (Par_Exn exns) = SOME exns
    3.38 +  | par_exns exn = if Exn.is_interrupt exn then NONE else SOME [#2 (serial exn)];
    3.39 +
    3.40 +fun make exns =
    3.41 +  (case map_filter par_exns exns of
    3.42 +    [] => Exn.Interrupt
    3.43 +  | e :: es => Par_Exn (Library.foldl (Ord_List.merge exn_ord) (e, es)));
    3.44 +
    3.45 +fun dest (Par_Exn exns) = SOME (rev exns)
    3.46 +  | dest _ = NONE;
    3.47 +
    3.48 +
    3.49 +(* parallel results *)
    3.50 +
    3.51 +fun all_res results = forall (fn Exn.Res _ => true | _ => false) results;
    3.52 +
    3.53 +fun release_all results =
    3.54 +  if all_res results then map Exn.release results
    3.55 +  else raise make (map_filter Exn.get_exn results);
    3.56 +
    3.57 +fun release_first results =
    3.58 +  if all_res results then map Exn.release results
    3.59 +  else
    3.60 +    (case get_first
    3.61 +        (fn res => if Exn.is_interrupt_exn res then NONE else Exn.get_exn res) results of
    3.62 +      NONE => Exn.interrupt ()
    3.63 +    | SOME exn => reraise exn);
    3.64 +
    3.65 +end;
    3.66 +
     4.1 --- a/src/Pure/Concurrent/par_list.ML	Wed Aug 17 15:03:30 2011 -0700
     4.2 +++ b/src/Pure/Concurrent/par_list.ML	Wed Aug 17 15:12:34 2011 -0700
     4.3 @@ -41,7 +41,7 @@
     4.4          handle exn => (if Exn.is_interrupt exn then Future.cancel_group group else (); reraise exn);
     4.5      in results end;
     4.6  
     4.7 -fun map_name name f xs = Exn.release_first (managed_results name f xs);
     4.8 +fun map_name name f xs = Par_Exn.release_first (managed_results name f xs);
     4.9  fun map f = map_name "Par_List.map" f;
    4.10  
    4.11  fun get_some f xs =
    4.12 @@ -55,7 +55,7 @@
    4.13    in
    4.14      (case get_first found results of
    4.15        SOME y => SOME y
    4.16 -    | NONE => (Exn.release_first results; NONE))
    4.17 +    | NONE => (Par_Exn.release_first results; NONE))
    4.18    end;
    4.19  
    4.20  fun find_some P = get_some (fn x => if P x then SOME x else NONE);
     5.1 --- a/src/Pure/Concurrent/task_queue.ML	Wed Aug 17 15:03:30 2011 -0700
     5.2 +++ b/src/Pure/Concurrent/task_queue.ML	Wed Aug 17 15:12:34 2011 -0700
     5.3 @@ -12,7 +12,7 @@
     5.4    val eq_group: group * group -> bool
     5.5    val cancel_group: group -> exn -> unit
     5.6    val is_canceled: group -> bool
     5.7 -  val group_status: group -> exn list
     5.8 +  val group_status: group -> exn option
     5.9    val str_of_group: group -> string
    5.10    val str_of_groups: group -> string
    5.11    type task
    5.12 @@ -56,12 +56,12 @@
    5.13  abstype group = Group of
    5.14   {parent: group option,
    5.15    id: int,
    5.16 -  status: exn list Synchronized.var}
    5.17 +  status: exn option Synchronized.var}
    5.18  with
    5.19  
    5.20  fun make_group (parent, id, status) = Group {parent = parent, id = id, status = status};
    5.21  
    5.22 -fun new_group parent = make_group (parent, new_id (), Synchronized.var "group" []);
    5.23 +fun new_group parent = make_group (parent, new_id (), Synchronized.var "group_status" NONE);
    5.24  
    5.25  fun group_id (Group {id, ...}) = id;
    5.26  fun eq_group (group1, group2) = group_id group1 = group_id group2;
    5.27 @@ -74,17 +74,20 @@
    5.28  
    5.29  fun cancel_group (Group {status, ...}) exn =
    5.30    Synchronized.change status
    5.31 -    (fn exns =>
    5.32 -      if not (Exn.is_interrupt exn) orelse null exns then exn :: exns
    5.33 -      else exns);
    5.34 +    (fn exns => SOME (Par_Exn.make (exn :: the_list exns)));
    5.35  
    5.36  fun is_canceled (Group {parent, status, ...}) =
    5.37 -  not (null (Synchronized.value status)) orelse
    5.38 +  is_some (Synchronized.value status) orelse
    5.39      (case parent of NONE => false | SOME group => is_canceled group);
    5.40  
    5.41 -fun group_status (Group {parent, status, ...}) =
    5.42 -  Synchronized.value status @
    5.43 -    (case parent of NONE => [] | SOME group => group_status group);
    5.44 +fun group_exns (Group {parent, status, ...}) =
    5.45 +  the_list (Synchronized.value status) @
    5.46 +    (case parent of NONE => [] | SOME group => group_exns group);
    5.47 +
    5.48 +fun group_status group =
    5.49 +  (case group_exns group of
    5.50 +    [] => NONE
    5.51 +  | exns => SOME (Par_Exn.make exns));
    5.52  
    5.53  fun str_of_group group =
    5.54    (is_canceled group ? enclose "(" ")") (string_of_int (group_id group));
     6.1 --- a/src/Pure/General/exn.ML	Wed Aug 17 15:03:30 2011 -0700
     6.2 +++ b/src/Pure/General/exn.ML	Wed Aug 17 15:12:34 2011 -0700
     6.3 @@ -11,7 +11,6 @@
     6.4    val get_exn: 'a result -> exn option
     6.5    val capture: ('a -> 'b) -> 'a -> 'b result
     6.6    val release: 'a result -> 'a
     6.7 -  val flat_result: 'a result result -> 'a result
     6.8    val map_result: ('a -> 'b) -> 'a result -> 'b result
     6.9    val maps_result: ('a -> 'b result) -> 'a result -> 'b result
    6.10    exception Interrupt
    6.11 @@ -21,10 +20,6 @@
    6.12    val is_interrupt_exn: 'a result -> bool
    6.13    val interruptible_capture: ('a -> 'b) -> 'a -> 'b result
    6.14    exception EXCEPTIONS of exn list
    6.15 -  val flatten: exn -> exn list
    6.16 -  val flatten_list: exn list -> exn list
    6.17 -  val release_all: 'a result list -> 'a list
    6.18 -  val release_first: 'a result list -> 'a list
    6.19  end;
    6.20  
    6.21  structure Exn: EXN =
    6.22 @@ -47,13 +42,10 @@
    6.23  fun release (Res y) = y
    6.24    | release (Exn e) = reraise e;
    6.25  
    6.26 -fun flat_result (Res x) = x
    6.27 -  | flat_result (Exn e) = Exn e;
    6.28 -
    6.29  fun map_result f (Res x) = Res (f x)
    6.30    | map_result f (Exn e) = Exn e;
    6.31  
    6.32 -fun maps_result f = flat_result o map_result f;
    6.33 +fun maps_result f = (fn Res x => x | Exn e => Exn e) o map_result f;
    6.34  
    6.35  
    6.36  (* interrupts *)
    6.37 @@ -75,23 +67,10 @@
    6.38    Res (f x) handle e => if is_interrupt e then reraise e else Exn e;
    6.39  
    6.40  
    6.41 -(* nested exceptions *)
    6.42 +(* concatenated exceptions *)
    6.43  
    6.44  exception EXCEPTIONS of exn list;
    6.45  
    6.46 -fun flatten (EXCEPTIONS exns) = flatten_list exns
    6.47 -  | flatten exn = if is_interrupt exn then [] else [exn]
    6.48 -and flatten_list exns = List.concat (map flatten exns);
    6.49 -
    6.50 -fun release_all results =
    6.51 -  if List.all (fn Res _ => true | _ => false) results
    6.52 -  then map (fn Res x => x) results
    6.53 -  else raise EXCEPTIONS (flatten_list (List.mapPartial get_exn results));
    6.54 -
    6.55 -fun release_first results = release_all results
    6.56 -  handle EXCEPTIONS [] => interrupt ()
    6.57 -    | EXCEPTIONS (exn :: _) => reraise exn;
    6.58 -
    6.59  end;
    6.60  
    6.61  datatype illegal = Interrupt;
     7.1 --- a/src/Pure/IsaMakefile	Wed Aug 17 15:03:30 2011 -0700
     7.2 +++ b/src/Pure/IsaMakefile	Wed Aug 17 15:12:34 2011 -0700
     7.3 @@ -60,6 +60,7 @@
     7.4    Concurrent/lazy.ML					\
     7.5    Concurrent/lazy_sequential.ML				\
     7.6    Concurrent/mailbox.ML					\
     7.7 +  Concurrent/par_exn.ML					\
     7.8    Concurrent/par_list.ML				\
     7.9    Concurrent/par_list_sequential.ML			\
    7.10    Concurrent/simple_thread.ML				\
     8.1 --- a/src/Pure/Isar/runtime.ML	Wed Aug 17 15:03:30 2011 -0700
     8.2 +++ b/src/Pure/Isar/runtime.ML	Wed Aug 17 15:12:34 2011 -0700
     8.3 @@ -60,34 +60,38 @@
     8.4      fun exn_msgs context exn =
     8.5        if Exn.is_interrupt exn then []
     8.6        else
     8.7 -        (case exn of
     8.8 -          Exn.EXCEPTIONS exns => maps (exn_msgs context) exns
     8.9 -        | CONTEXT (ctxt, exn) => exn_msgs (SOME ctxt) exn
    8.10 -        | EXCURSION_FAIL (exn, loc) =>
    8.11 -            map (fn msg => msg ^ Markup.markup Markup.no_report ("\n" ^ loc)) (exn_msgs context exn)
    8.12 -        | TERMINATE => ["Exit"]
    8.13 -        | TimeLimit.TimeOut => ["Timeout"]
    8.14 -        | TOPLEVEL_ERROR => ["Error"]
    8.15 -        | ERROR msg => [msg]
    8.16 -        | Fail msg => [raised exn "Fail" [msg]]
    8.17 -        | THEORY (msg, thys) =>
    8.18 -            [raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))]
    8.19 -        | Ast.AST (msg, asts) =>
    8.20 -            [raised exn "AST" (msg ::
    8.21 -              (if detailed then map (Pretty.string_of o Ast.pretty_ast) asts else []))]
    8.22 -        | TYPE (msg, Ts, ts) =>
    8.23 -            [raised exn "TYPE" (msg ::
    8.24 -              (if detailed then
    8.25 -                if_context context Syntax.string_of_typ Ts @
    8.26 -                if_context context Syntax.string_of_term ts
    8.27 -               else []))]
    8.28 -        | TERM (msg, ts) =>
    8.29 -            [raised exn "TERM" (msg ::
    8.30 -              (if detailed then if_context context Syntax.string_of_term ts else []))]
    8.31 -        | THM (msg, i, thms) =>
    8.32 -            [raised exn ("THM " ^ string_of_int i) (msg ::
    8.33 -              (if detailed then if_context context Display.string_of_thm thms else []))]
    8.34 -        | _ => [raised exn (General.exnMessage exn) []]);
    8.35 +        (case Par_Exn.dest exn of
    8.36 +          SOME exns => maps (exn_msgs context) exns
    8.37 +        | NONE =>
    8.38 +            (case exn of
    8.39 +              Exn.EXCEPTIONS exns => maps (exn_msgs context) exns
    8.40 +            | CONTEXT (ctxt, exn) => exn_msgs (SOME ctxt) exn
    8.41 +            | EXCURSION_FAIL (exn, loc) =>
    8.42 +                map (fn msg => msg ^ Markup.markup Markup.no_report ("\n" ^ loc))
    8.43 +                  (exn_msgs context exn)
    8.44 +            | TERMINATE => ["Exit"]
    8.45 +            | TimeLimit.TimeOut => ["Timeout"]
    8.46 +            | TOPLEVEL_ERROR => ["Error"]
    8.47 +            | ERROR msg => [msg]
    8.48 +            | Fail msg => [raised exn "Fail" [msg]]
    8.49 +            | THEORY (msg, thys) =>
    8.50 +                [raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))]
    8.51 +            | Ast.AST (msg, asts) =>
    8.52 +                [raised exn "AST" (msg ::
    8.53 +                  (if detailed then map (Pretty.string_of o Ast.pretty_ast) asts else []))]
    8.54 +            | TYPE (msg, Ts, ts) =>
    8.55 +                [raised exn "TYPE" (msg ::
    8.56 +                  (if detailed then
    8.57 +                    if_context context Syntax.string_of_typ Ts @
    8.58 +                    if_context context Syntax.string_of_term ts
    8.59 +                   else []))]
    8.60 +            | TERM (msg, ts) =>
    8.61 +                [raised exn "TERM" (msg ::
    8.62 +                  (if detailed then if_context context Syntax.string_of_term ts else []))]
    8.63 +            | THM (msg, i, thms) =>
    8.64 +                [raised exn ("THM " ^ string_of_int i) (msg ::
    8.65 +                  (if detailed then if_context context Display.string_of_thm thms else []))]
    8.66 +            | _ => [raised exn (General.exnMessage exn) []]));
    8.67    in exn_msgs NONE e end;
    8.68  
    8.69  fun exn_message exn_position exn =
     9.1 --- a/src/Pure/ML-Systems/polyml-5.2.1.ML	Wed Aug 17 15:03:30 2011 -0700
     9.2 +++ b/src/Pure/ML-Systems/polyml-5.2.1.ML	Wed Aug 17 15:12:34 2011 -0700
     9.3 @@ -13,6 +13,8 @@
     9.4  end;
     9.5  
     9.6  fun reraise exn = raise exn;
     9.7 +fun set_exn_serial (_: int) (exn: exn) = exn;
     9.8 +fun get_exn_serial (exn: exn) : int option = NONE;
     9.9  
    9.10  use "ML-Systems/polyml_common.ML";
    9.11  use "ML-Systems/multithreading_polyml.ML";
    10.1 --- a/src/Pure/ML-Systems/polyml.ML	Wed Aug 17 15:03:30 2011 -0700
    10.2 +++ b/src/Pure/ML-Systems/polyml.ML	Wed Aug 17 15:12:34 2011 -0700
    10.3 @@ -17,6 +17,22 @@
    10.4      NONE => raise exn
    10.5    | SOME location => PolyML.raiseWithLocation (exn, location));
    10.6  
    10.7 +fun set_exn_serial i exn =
    10.8 +  let
    10.9 +    val (file, startLine, endLine) =
   10.10 +      (case PolyML.exceptionLocation exn of
   10.11 +        NONE => ("", 0, 0)
   10.12 +      | SOME {file, startLine, endLine, startPosition, ...} => (file, startLine, endLine));
   10.13 +    val location =
   10.14 +      {file = file, startLine = startLine, endLine = endLine,
   10.15 +        startPosition = ~ i, endPosition = 0};
   10.16 +  in PolyML.raiseWithLocation (exn, location) handle e => e end;
   10.17 +
   10.18 +fun get_exn_serial exn =
   10.19 +  (case Option.map #startPosition (PolyML.exceptionLocation exn) of
   10.20 +    NONE => NONE
   10.21 +  | SOME i => if i >= 0 then NONE else SOME (~ i));
   10.22 +
   10.23  use "ML-Systems/polyml_common.ML";
   10.24  use "ML-Systems/multithreading_polyml.ML";
   10.25  use "ML-Systems/unsynchronized.ML";
    11.1 --- a/src/Pure/ML-Systems/smlnj.ML	Wed Aug 17 15:03:30 2011 -0700
    11.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Wed Aug 17 15:12:34 2011 -0700
    11.3 @@ -3,10 +3,13 @@
    11.4  Compatibility file for Standard ML of New Jersey 110 or later.
    11.5  *)
    11.6  
    11.7 +use "ML-Systems/proper_int.ML";
    11.8 +
    11.9  exception Interrupt;
   11.10  fun reraise exn = raise exn;
   11.11 +fun set_exn_serial (_: int) (exn: exn) = exn;
   11.12 +fun get_exn_serial (exn: exn) : int option = NONE;
   11.13  
   11.14 -use "ML-Systems/proper_int.ML";
   11.15  use "ML-Systems/overloading_smlnj.ML";
   11.16  use "General/exn.ML";
   11.17  use "ML-Systems/single_assignment.ML";
    12.1 --- a/src/Pure/PIDE/document.ML	Wed Aug 17 15:03:30 2011 -0700
    12.2 +++ b/src/Pure/PIDE/document.ML	Wed Aug 17 15:12:34 2011 -0700
    12.3 @@ -372,7 +372,7 @@
    12.4                          |> set_result result;
    12.5                      in ((assigns, execs, [(name, node')]), node') end)
    12.6                end))
    12.7 -      |> Future.join_results |> Exn.release_all |> map #1;
    12.8 +      |> Future.join_results |> Par_Exn.release_all |> map #1;
    12.9  
   12.10      val state' = state
   12.11        |> fold (fold define_exec o #2) updates
    13.1 --- a/src/Pure/ROOT.ML	Wed Aug 17 15:03:30 2011 -0700
    13.2 +++ b/src/Pure/ROOT.ML	Wed Aug 17 15:12:34 2011 -0700
    13.3 @@ -77,7 +77,7 @@
    13.4  then use "Concurrent/bash.ML"
    13.5  else use "Concurrent/bash_sequential.ML";
    13.6  
    13.7 -use "Concurrent/mailbox.ML";
    13.8 +use "Concurrent/par_exn.ML";
    13.9  use "Concurrent/task_queue.ML";
   13.10  use "Concurrent/future.ML";
   13.11  
   13.12 @@ -89,6 +89,7 @@
   13.13  if Multithreading.available then ()
   13.14  else use "Concurrent/par_list_sequential.ML";
   13.15  
   13.16 +use "Concurrent/mailbox.ML";
   13.17  use "Concurrent/cache.ML";
   13.18  
   13.19  
    14.1 --- a/src/Pure/Thy/thy_info.ML	Wed Aug 17 15:03:30 2011 -0700
    14.2 +++ b/src/Pure/Thy/thy_info.ML	Wed Aug 17 15:12:34 2011 -0700
    14.3 @@ -207,7 +207,7 @@
    14.4                    " (unresolved " ^ commas_quote (map #1 bad) ^ ")") [])))
    14.5      | Finished thy => Future.value (thy, Future.value (), I)))
    14.6    #> maps (fn result => (finish_thy (Future.join result); []) handle exn => [Exn.Exn exn])
    14.7 -  #> rev #> Exn.release_all) #> ignore;
    14.8 +  #> rev #> Par_Exn.release_all) #> ignore;
    14.9  
   14.10  in
   14.11  
    15.1 --- a/src/Pure/thm.ML	Wed Aug 17 15:03:30 2011 -0700
    15.2 +++ b/src/Pure/thm.ML	Wed Aug 17 15:12:34 2011 -0700
    15.3 @@ -515,7 +515,7 @@
    15.4  fun fulfill_body (Thm (Deriv {promises, body}, {thy_ref, ...})) =
    15.5    Proofterm.fulfill_norm_proof (Theory.deref thy_ref)
    15.6      (map #1 promises ~~ fulfill_bodies (map #2 promises)) body
    15.7 -and fulfill_bodies futures = map fulfill_body (Exn.release_all (Future.join_results futures));
    15.8 +and fulfill_bodies futures = map fulfill_body (Par_Exn.release_all (Future.join_results futures));
    15.9  
   15.10  val join_proofs = Proofterm.join_bodies o map fulfill_body;
   15.11