added Future.joins convenience;
clarified Future.map: based on Future.cond_forks;

--- a/src/Pure/Concurrent/future.ML	Sat Aug 20 09:42:34 2011 +0200
+++ b/src/Pure/Concurrent/future.ML	Sat Aug 20 15:52:29 2011 +0200
@@ -62,12 +62,13 @@
   val fork: (unit -> 'a) -> 'a future
   val join_results: 'a future list -> 'a Exn.result list
   val join_result: 'a future -> 'a Exn.result
+  val joins: 'a future list -> 'a list
   val join: 'a future -> 'a
   val join_tasks: task list -> unit
   val value_result: 'a Exn.result -> 'a future
   val value: 'a -> 'a future
+  val cond_forks: fork_params -> (unit -> 'a) list -> 'a future list
   val map: ('a -> 'b) -> 'a future -> 'b future
-  val cond_forks: fork_params -> (unit -> 'a) list -> 'a future list
   val promise_group: group -> (unit -> unit) -> 'a future
   val promise: (unit -> unit) -> 'a future
   val fulfill_result: 'a future -> 'a Exn.result -> unit
@@ -534,6 +535,7 @@
 end;
 
 fun join_result x = singleton join_results x;
+fun joins xs = Par_Exn.release_all (join_results xs);
 fun join x = Exn.release (join_result x);
 
 fun join_tasks [] = ()
@@ -556,6 +558,10 @@
 
 fun value x = value_result (Exn.Res x);
 
+fun cond_forks args es =
+  if Multithreading.enabled () then forks args es
+  else map (fn e => value_result (Exn.interruptible_capture e ())) es;
+
 fun map_future f x =
   let
     val task = task_of x;
@@ -569,16 +575,12 @@
   in
     if extended then Future {promised = false, task = task, result = result}
     else
-      (singleton o forks)
+      (singleton o cond_forks)
         {name = "map_future", group = SOME group, deps = [task],
           pri = Task_Queue.pri_of_task task, interrupts = true}
         (fn () => f (join x))
   end;
 
-fun cond_forks args es =
-  if Multithreading.enabled () then forks args es
-  else map (fn e => value_result (Exn.interruptible_capture e ())) es;
-
 
 (* promised futures -- fulfilled by external means *)
 

--- a/src/Pure/PIDE/document.ML	Sat Aug 20 09:42:34 2011 +0200
+++ b/src/Pure/PIDE/document.ML	Sat Aug 20 15:52:29 2011 +0200
@@ -371,7 +371,7 @@
                         |> set_result result;
                     in ((assigns, execs, [(name, node')]), node') end)
               end))
-      |> Future.join_results |> Par_Exn.release_all |> map #1;
+      |> Future.joins |> map #1;
 
     val state' = state
       |> fold (fold define_exec o #2) updates

--- a/src/Pure/proofterm.ML	Sat Aug 20 09:42:34 2011 +0200
+++ b/src/Pure/proofterm.ML	Sat Aug 20 15:52:29 2011 +0200
@@ -171,8 +171,7 @@
 type oracle = string * term;
 type pthm = serial * (string * term * proof_body future);
 
-fun join_thm (pthm: pthm) = ignore (Future.join (#3 (#2 pthm)));
-fun join_thms thms = (Future.join_results (map (#3 o #2) thms); List.app join_thm thms);
+fun join_thms thms = ignore (Future.joins (map (#3 o #2) thms));
 fun join_body (PBody {thms, ...}) = join_thms thms;
 
 fun proof_of (PBody {proof, ...}) = proof;

--- a/src/Pure/thm.ML	Sat Aug 20 09:42:34 2011 +0200
+++ b/src/Pure/thm.ML	Sat Aug 20 15:52:29 2011 +0200
@@ -515,7 +515,7 @@
 fun fulfill_body (Thm (Deriv {promises, body}, {thy_ref, ...})) =
   Proofterm.fulfill_norm_proof (Theory.deref thy_ref)
     (map #1 promises ~~ fulfill_bodies (map #2 promises)) body
-and fulfill_bodies futures = map fulfill_body (Par_Exn.release_all (Future.join_results futures));
+and fulfill_bodies futures = map fulfill_body (Future.joins futures);
 
 fun join_proofs thms = ignore (map fulfill_body thms);