join_results: allow CRITICAL join of finished futures;
authorwenzelm
Tue Oct 21 16:53:00 2008 +0200 (2008-10-21)
changeset 286478068cdc84e7e
parent 28646 3a8d75c935ce
child 28648 4889b48919a0
join_results: allow CRITICAL join of finished futures;
added singleton join_result;
src/Pure/Concurrent/future.ML
     1.1 --- a/src/Pure/Concurrent/future.ML	Tue Oct 21 16:52:59 2008 +0200
     1.2 +++ b/src/Pure/Concurrent/future.ML	Tue Oct 21 16:53:00 2008 +0200
     1.3 @@ -40,6 +40,7 @@
     1.4    val fork: (unit -> 'a) -> 'a T
     1.5    val fork_background: (unit -> 'a) -> 'a T
     1.6    val join_results: 'a T list -> 'a Exn.result list
     1.7 +  val join_result: 'a T -> 'a Exn.result
     1.8    val join: 'a T -> 'a
     1.9    val focus: task list -> unit
    1.10    val interrupt_task: string -> unit
    1.11 @@ -258,6 +259,7 @@
    1.12        let
    1.13          val _ = scheduler_check "join check";
    1.14          val _ = Multithreading.self_critical () andalso
    1.15 +          exists (not o is_finished) xs andalso
    1.16            error "Cannot join future values within critical section";
    1.17  
    1.18          fun join_loop _ [] = ()
    1.19 @@ -287,7 +289,8 @@
    1.20  
    1.21        in xs |> map (fn Future {result = ref (SOME res), ...} => res) end) ();
    1.22  
    1.23 -fun join x = Exn.release (singleton join_results x);
    1.24 +fun join_result x = singleton join_results x;
    1.25 +fun join x = Exn.release (join_result x);
    1.26  
    1.27  
    1.28  (* misc operations *)