src/Pure/Concurrent/par_list.ML
changeset 28646 3a8d75c935ce
parent 28645 605a3b1ef6ba
child 28980 9d7ea903e877
equal deleted inserted replaced
28645:605a3b1ef6ba 28646:3a8d75c935ce
    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.future (SOME group) [] true (fn () => f x)) xs;
    35       val _ = List.app (ignore o Future.join_results o single) 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);
    40 
    40