# HG changeset patch
# User wenzelm
# Date 1223578396 -7200
# Node ID 78affc7d4d0f3c4ca8554332952ecf7637c1cd6c
# Parent  003f52c2bb8fc48c3d93ab18b482ff2ada096f0d
subject to Multithreading.enabled;
raw_map: join sequentially, less overhead;

diff -r 003f52c2bb8f -r 78affc7d4d0f src/Pure/Concurrent/par_list.ML
--- a/src/Pure/Concurrent/par_list.ML	Thu Oct 09 20:53:15 2008 +0200
+++ b/src/Pure/Concurrent/par_list.ML	Thu Oct 09 20:53:16 2008 +0200
@@ -28,9 +28,13 @@
 struct
 
 fun raw_map f xs =
-  let val group = TaskQueue.new_group () in
-    Future.join_results (List.map (fn x => Future.future (SOME group) [] true (fn () => f x)) xs)
-  end;
+  if ! future_scheduler andalso Multithreading.enabled () then
+    let
+      val group = TaskQueue.new_group ();
+      val futures = map (fn x => Future.future (SOME group) [] true (fn () => f x)) xs;
+      val _ = List.app (ignore o Future.join_results o single) futures;
+    in Future.join_results futures end
+  else map (Exn.capture f) xs;
 
 fun map f xs = Exn.release_first (raw_map f xs);