# HG changeset patch
# User wenzelm
# Date 1221076230 -7200
# Node ID 7ed74d0ba6077b1a461f79fc91f34cc083db6537
# Parent  6d977729c8fadf19456c0d3cd09d63844c35866e
replaced join_all by join_results, which returns Exn.results;
join: disallow Multithreading.self_critical, which is prone to deadlocks due to context change via fork;

diff -r 6d977729c8fa -r 7ed74d0ba607 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Wed Sep 10 20:28:01 2008 +0200
+++ b/src/Pure/Concurrent/future.ML	Wed Sep 10 21:50:30 2008 +0200
@@ -16,7 +16,7 @@
   val future: group option -> task list -> (unit -> 'a) -> 'a T
   val fork: (unit -> 'a) -> 'a T
   val cancel: 'a T -> unit
-  val join_all: 'a T list -> 'a list
+  val join_results: 'a T list -> 'a Exn.result list
   val join: 'a T -> 'a
 end;
 
@@ -212,8 +212,10 @@
 
 (* join: retrieve results *)
 
-fun join_all xs =
+fun join_results xs =
   let
+    val _ = Multithreading.self_critical () andalso
+      error "Cannot join future values within critical section";
     val _ = scheduler_check ();
 
     fun unfinished () =
@@ -238,14 +240,9 @@
       | SOME (task, _) => SYNCHRONIZED "join" (fn () =>
          (change queue (TaskQueue.depend (unfinished ()) task); active_join ())));
 
-    val res = xs |> map (fn Future {result = ref (SOME res), ...} => res);
-  in
-    (case get_first (fn Exn.Exn Interrupt => NONE | Exn.Exn e => SOME e | _ => NONE) res of
-      NONE => map Exn.release res
-    | SOME e => raise e)
-  end;
+  in xs |> map (fn Future {result = ref (SOME res), ...} => res) end;
 
-fun join x = singleton join_all x;
+fun join x = Exn.release (singleton join_results x);
 
 
 (* termination *)