src/Pure/Concurrent/par_list.ML
changeset 28980 9d7ea903e877
parent 28646 3a8d75c935ce
child 29120 8a904ff43f28
equal deleted inserted replaced
28979:3ce619d8d432 28980:9d7ea903e877
    29 
    29 
    30 fun raw_map f xs =
    30 fun raw_map f xs =
    31   if Future.enabled () then
    31   if Future.enabled () then
    32     let
    32     let
    33       val group = TaskQueue.new_group ();
    33       val group = TaskQueue.new_group ();
    34       val futures = map (fn x => Future.future (SOME group) [] true (fn () => f x)) xs;
    34       val futures = map (fn x => Future.fork_group group (fn () => f x)) xs;
    35       val _ = List.app (ignore o Future.join_result) futures;
    35       val _ = List.app (ignore o Future.join_result) futures;
    36     in Future.join_results futures end
    36     in Future.join_results futures end
    37   else map (Exn.capture f) xs;
    37   else map (Exn.capture f) xs;
    38 
    38 
    39 fun map f xs = Exn.release_first (raw_map f xs);
    39 fun map f xs = Exn.release_first (raw_map f xs);