equal
deleted
inserted
replaced
25 |
25 |
26 structure Par_List: PAR_LIST = |
26 structure Par_List: PAR_LIST = |
27 struct |
27 struct |
28 |
28 |
29 fun raw_map f xs = |
29 fun raw_map f xs = |
30 let val group = Task_Queue.new_group (Future.worker_group ()) |
30 if Multithreading.enabled () then |
31 in Future.join_results (map (fn x => Future.fork_group group (fn () => f x)) xs) end; |
31 let val group = Task_Queue.new_group (Future.worker_group ()) |
|
32 in Future.join_results (map (fn x => Future.fork_group group (fn () => f x)) xs) end |
|
33 else map (Exn.capture f) xs; |
32 |
34 |
33 fun map f xs = Exn.release_first (raw_map f xs); |
35 fun map f xs = Exn.release_first (raw_map f xs); |
34 |
36 |
35 fun get_some f xs = |
37 fun get_some f xs = |
36 let |
38 let |