# HG changeset patch
# User wenzelm
# Date 1224600780 -7200
# Node ID 8068cdc84e7e925c89b1fa574e6747e490e946f3
# Parent  3a8d75c935ce150db2f9f88cf350ae4a27de65b2
join_results: allow CRITICAL join of finished futures;
added singleton join_result;

diff -r 3a8d75c935ce -r 8068cdc84e7e src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Tue Oct 21 16:52:59 2008 +0200
+++ b/src/Pure/Concurrent/future.ML	Tue Oct 21 16:53:00 2008 +0200
@@ -40,6 +40,7 @@
   val fork: (unit -> 'a) -> 'a T
   val fork_background: (unit -> 'a) -> 'a T
   val join_results: 'a T list -> 'a Exn.result list
+  val join_result: 'a T -> 'a Exn.result
   val join: 'a T -> 'a
   val focus: task list -> unit
   val interrupt_task: string -> unit
@@ -258,6 +259,7 @@
       let
         val _ = scheduler_check "join check";
         val _ = Multithreading.self_critical () andalso
+          exists (not o is_finished) xs andalso
           error "Cannot join future values within critical section";
 
         fun join_loop _ [] = ()
@@ -287,7 +289,8 @@
 
       in xs |> map (fn Future {result = ref (SOME res), ...} => res) end) ();
 
-fun join x = Exn.release (singleton join_results x);
+fun join_result x = singleton join_results x;
+fun join x = Exn.release (join_result x);
 
 
 (* misc operations *)