# HG changeset patch
# User wenzelm
# Date 1222177733 -7200
# Node ID 33d58fdc177df08ac45b56382bd972ba0c7097b1
# Parent  7e803c3923420be931108649afcf832be29b65e0
join_results: special case for empty list, works without multithreading;

diff -r 7e803c392342 -r 33d58fdc177d src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Tue Sep 23 15:48:52 2008 +0200
+++ b/src/Pure/Concurrent/future.ML	Tue Sep 23 15:48:53 2008 +0200
@@ -235,35 +235,36 @@
 
 (* join: retrieve results *)
 
-fun join_results xs =
-  let
-    val _ = scheduler_check ();
-    val _ = Multithreading.self_critical () andalso
-      error "Cannot join future values within critical section";
+fun join_results [] = []
+  | join_results xs =
+      let
+        val _ = scheduler_check ();
+        val _ = Multithreading.self_critical () andalso
+          error "Cannot join future values within critical section";
 
-    fun unfinished () =
-      xs |> map_filter (fn Future {task, result = ref NONE, ...} => SOME task | _ => NONE);
+        fun unfinished () =
+          xs |> map_filter (fn Future {task, result = ref NONE, ...} => SOME task | _ => NONE);
 
-    (*alien thread -- refrain from contending for resources*)
-    fun passive_join () = (*requires SYNCHRONIZED*)
-      (case unfinished () of [] => ()
-      | _ => (wait "passive_join"; passive_join ()));
+        (*alien thread -- refrain from contending for resources*)
+        fun passive_join () = (*requires SYNCHRONIZED*)
+          (case unfinished () of [] => ()
+          | _ => (wait "passive_join"; passive_join ()));
 
-    (*proper worker thread -- actively work towards results*)
-    fun active_join () = (*requires SYNCHRONIZED*)
-      (case unfinished () of [] => ()
-      | tasks =>
-          (case change_result queue (TaskQueue.dequeue_towards tasks) of
-            NONE => (worker_wait "active_join"; active_join ())
-          | SOME work => (execute "active_join" work; active_join ())));
+        (*proper worker thread -- actively work towards results*)
+        fun active_join () = (*requires SYNCHRONIZED*)
+          (case unfinished () of [] => ()
+          | tasks =>
+              (case change_result queue (TaskQueue.dequeue_towards tasks) of
+                NONE => (worker_wait "active_join"; active_join ())
+              | SOME work => (execute "active_join" work; active_join ())));
 
-    val _ =
-      (case thread_data () of
-        NONE => SYNCHRONIZED "passive_join" passive_join
-      | SOME (task, _) => SYNCHRONIZED "active_join" (fn () =>
-         (change queue (TaskQueue.depend (unfinished ()) task); active_join ())));
+        val _ =
+          (case thread_data () of
+            NONE => SYNCHRONIZED "passive_join" passive_join
+          | SOME (task, _) => SYNCHRONIZED "active_join" (fn () =>
+             (change queue (TaskQueue.depend (unfinished ()) task); active_join ())));
 
-  in xs |> map (fn Future {result = ref (SOME res), ...} => res) end;
+      in xs |> map (fn Future {result = ref (SOME res), ...} => res) end;
 
 fun join x = Exn.release (singleton join_results x);