src/Pure/Concurrent/par_list.ML
changeset 28645 605a3b1ef6ba
parent 28549 78affc7d4d0f
child 28646 3a8d75c935ce
equal deleted inserted replaced
28644:e2ae4a6cf166 28645:605a3b1ef6ba
    26 
    26 
    27 structure ParList: PAR_LIST =
    27 structure ParList: PAR_LIST =
    28 struct
    28 struct
    29 
    29 
    30 fun raw_map f xs =
    30 fun raw_map f xs =
    31   if ! future_scheduler andalso Multithreading.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_results o single) futures;
    36     in Future.join_results futures end
    36     in Future.join_results futures end