author | wenzelm |
Sat, 27 Feb 2010 13:31:55 +0100 | |
changeset 35393 | 2f83aa48d696 |
parent 35392 | 5da5ac6c6b77 |
child 35394 | 11f58c600707 |
--- a/src/Pure/Concurrent/par_list.ML Fri Feb 26 23:08:45 2010 +0100 +++ b/src/Pure/Concurrent/par_list.ML Sat Feb 27 13:31:55 2010 +0100 @@ -27,7 +27,7 @@ struct fun raw_map f xs = - if Multithreading.enabled () then + if Multithreading.enabled () andalso not (Multithreading.self_critical ()) then let val group = Task_Queue.new_group (Future.worker_group ()) in Future.join_results (map (fn x => Future.fork_group group (fn () => f x)) xs) end else map (Exn.capture f) xs;