diff -r 2f70b1ddd09f -r 1c191a39549f src/Pure/Concurrent/par_list.ML --- a/src/Pure/Concurrent/par_list.ML Mon Jan 31 21:54:49 2011 +0100 +++ b/src/Pure/Concurrent/par_list.ML Mon Jan 31 22:57:01 2011 +0100 @@ -26,18 +26,19 @@ structure Par_List: PAR_LIST = struct -fun managed_results f xs = +fun managed_results name f xs = if Multithreading.enabled () andalso not (Multithreading.self_critical ()) then let val group = Task_Queue.new_group (Future.worker_group ()); val futures = - Future.bulk {group = SOME group, deps = [], pri = 0} (map (fn x => fn () => f x) xs); + Future.bulk {name = name, group = SOME group, deps = [], pri = 0} + (map (fn x => fn () => f x) xs); val results = Future.join_results futures handle exn => (if Exn.is_interrupt exn then Future.cancel_group group else (); reraise exn); in results end else map (Exn.capture f) xs; -fun map f xs = Exn.release_first (managed_results f xs); +fun map f xs = Exn.release_first (managed_results "Par_List.map" f xs); fun get_some f xs = let @@ -45,7 +46,8 @@ fun found (Exn.Exn (FOUND some)) = some | found _ = NONE; val results = - managed_results (fn x => (case f x of NONE => () | some => raise FOUND some)) xs; + managed_results "Par_List.get_some" + (fn x => (case f x of NONE => () | some => raise FOUND some)) xs; in (case get_first found results of SOME y => SOME y