1.1 --- a/src/Pure/Concurrent/future.ML	Wed Nov 06 18:15:25 2013 +0100
     1.2 +++ b/src/Pure/Concurrent/future.ML	Wed Nov 06 20:46:00 2013 +0100
     1.3 @@ -68,6 +68,7 @@
     1.4    val join_result: 'a future -> 'a Exn.result
     1.5    val joins: 'a future list -> 'a list
     1.6    val join: 'a future -> 'a
     1.7 +  val join_tasks: task list -> unit
     1.8    val value_result: 'a Exn.result -> 'a future
     1.9    val value: 'a -> 'a future
    1.10    val cond_forks: params -> (unit -> 'a) list -> 'a future list
    1.11 @@ -76,6 +77,7 @@
    1.12    val promise: (unit -> unit) -> 'a future
    1.13    val fulfill_result: 'a future -> 'a Exn.result -> unit
    1.14    val fulfill: 'a future -> 'a -> unit
    1.15 +  val group_snapshot: group -> task list
    1.16    val terminate: group -> unit
    1.17    val shutdown: unit -> unit
    1.18  end;
    1.19 @@ -575,6 +577,14 @@
    1.20  fun joins xs = Par_Exn.release_all (join_results xs);
    1.21  fun join x = Exn.release (join_result x);
    1.22  
    1.23 +fun join_tasks tasks =
    1.24 +  if null tasks then ()
    1.25 +  else
    1.26 +    (singleton o forks)
    1.27 +      {name = "join_tasks", group = SOME (new_group NONE),
    1.28 +        deps = tasks, pri = 0, interrupts = false} I
    1.29 +    |> join;
    1.30 +
    1.31  
    1.32  (* fast-path operations -- bypass task queue if possible *)
    1.33  
    1.34 @@ -663,22 +673,20 @@
    1.35  fun fulfill x res = fulfill_result x (Exn.Res res);
    1.36  
    1.37  
    1.38 +(* group snapshot *)
    1.39 +
    1.40 +fun group_snapshot group =
    1.41 +  SYNCHRONIZED "group_snapshot" (fn () =>
    1.42 +    Task_Queue.group_tasks (! queue) group);
    1.43 +
    1.44 +
    1.45  (* terminate *)
    1.46  
    1.47  fun terminate group =
    1.48 -  let
    1.49 -    val tasks =
    1.50 -      SYNCHRONIZED "terminate" (fn () =>
    1.51 -        let val _ = cancel_group_unsynchronized group;
    1.52 -        in Task_Queue.group_tasks (! queue) group end);
    1.53 -  in
    1.54 -    if null tasks then ()
    1.55 -    else
    1.56 -      (singleton o forks)
    1.57 -        {name = "terminate", group = SOME (new_group NONE),
    1.58 -          deps = tasks, pri = 0, interrupts = false} I
    1.59 -      |> join
    1.60 -  end;
    1.61 +  SYNCHRONIZED "terminate" (fn () =>
    1.62 +    let val _ = cancel_group_unsynchronized group;
    1.63 +    in Task_Queue.group_tasks (! queue) group end)
    1.64 +  |> join_tasks;
    1.65  
    1.66  
    1.67  (* shutdown *)