1.1 --- a/src/Pure/Concurrent/future.ML	Tue Sep 23 15:48:52 2008 +0200
     1.2 +++ b/src/Pure/Concurrent/future.ML	Tue Sep 23 15:48:53 2008 +0200
     1.3 @@ -235,35 +235,36 @@
     1.4  
     1.5  (* join: retrieve results *)
     1.6  
     1.7 -fun join_results xs =
     1.8 -  let
     1.9 -    val _ = scheduler_check ();
    1.10 -    val _ = Multithreading.self_critical () andalso
    1.11 -      error "Cannot join future values within critical section";
    1.12 +fun join_results [] = []
    1.13 +  | join_results xs =
    1.14 +      let
    1.15 +        val _ = scheduler_check ();
    1.16 +        val _ = Multithreading.self_critical () andalso
    1.17 +          error "Cannot join future values within critical section";
    1.18  
    1.19 -    fun unfinished () =
    1.20 -      xs |> map_filter (fn Future {task, result = ref NONE, ...} => SOME task | _ => NONE);
    1.21 +        fun unfinished () =
    1.22 +          xs |> map_filter (fn Future {task, result = ref NONE, ...} => SOME task | _ => NONE);
    1.23  
    1.24 -    (*alien thread -- refrain from contending for resources*)
    1.25 -    fun passive_join () = (*requires SYNCHRONIZED*)
    1.26 -      (case unfinished () of [] => ()
    1.27 -      | _ => (wait "passive_join"; passive_join ()));
    1.28 +        (*alien thread -- refrain from contending for resources*)
    1.29 +        fun passive_join () = (*requires SYNCHRONIZED*)
    1.30 +          (case unfinished () of [] => ()
    1.31 +          | _ => (wait "passive_join"; passive_join ()));
    1.32  
    1.33 -    (*proper worker thread -- actively work towards results*)
    1.34 -    fun active_join () = (*requires SYNCHRONIZED*)
    1.35 -      (case unfinished () of [] => ()
    1.36 -      | tasks =>
    1.37 -          (case change_result queue (TaskQueue.dequeue_towards tasks) of
    1.38 -            NONE => (worker_wait "active_join"; active_join ())
    1.39 -          | SOME work => (execute "active_join" work; active_join ())));
    1.40 +        (*proper worker thread -- actively work towards results*)
    1.41 +        fun active_join () = (*requires SYNCHRONIZED*)
    1.42 +          (case unfinished () of [] => ()
    1.43 +          | tasks =>
    1.44 +              (case change_result queue (TaskQueue.dequeue_towards tasks) of
    1.45 +                NONE => (worker_wait "active_join"; active_join ())
    1.46 +              | SOME work => (execute "active_join" work; active_join ())));
    1.47  
    1.48 -    val _ =
    1.49 -      (case thread_data () of
    1.50 -        NONE => SYNCHRONIZED "passive_join" passive_join
    1.51 -      | SOME (task, _) => SYNCHRONIZED "active_join" (fn () =>
    1.52 -         (change queue (TaskQueue.depend (unfinished ()) task); active_join ())));
    1.53 +        val _ =
    1.54 +          (case thread_data () of
    1.55 +            NONE => SYNCHRONIZED "passive_join" passive_join
    1.56 +          | SOME (task, _) => SYNCHRONIZED "active_join" (fn () =>
    1.57 +             (change queue (TaskQueue.depend (unfinished ()) task); active_join ())));
    1.58  
    1.59 -  in xs |> map (fn Future {result = ref (SOME res), ...} => res) end;
    1.60 +      in xs |> map (fn Future {result = ref (SOME res), ...} => res) end;
    1.61  
    1.62  fun join x = Exn.release (singleton join_results x);
    1.63