equal
deleted
inserted
replaced
24 end; |
24 end; |
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 managed_results f xs = |
30 if Multithreading.enabled () andalso not (Multithreading.self_critical ()) then |
30 if Multithreading.enabled () andalso not (Multithreading.self_critical ()) then |
31 let val shared_group = Task_Queue.new_group (Future.worker_group ()) |
31 let |
32 in Future.join_results (map (fn x => Future.fork_group shared_group (fn () => f x)) xs) end |
32 val shared_group = Task_Queue.new_group (Future.worker_group ()); |
|
33 val results = |
|
34 Future.join_results (map (fn x => Future.fork_group shared_group (fn () => f x)) xs) |
|
35 handle exn => |
|
36 (if Exn.is_interrupt exn then Future.cancel_group shared_group else (); reraise exn); |
|
37 in results end |
33 else map (Exn.capture f) xs; |
38 else map (Exn.capture f) xs; |
34 |
39 |
35 fun map f xs = Exn.release_first (raw_map f xs); |
40 fun map f xs = Exn.release_first (managed_results f xs); |
36 |
41 |
37 fun get_some f xs = |
42 fun get_some f xs = |
38 let |
43 let |
39 exception FOUND of 'b option; |
44 exception FOUND of 'b option; |
40 fun found (Exn.Exn (FOUND some)) = some |
45 fun found (Exn.Exn (FOUND some)) = some |
41 | found _ = NONE; |
46 | found _ = NONE; |
42 val results = raw_map (fn x => (case f x of NONE => () | some => raise FOUND some)) xs; |
47 val results = |
|
48 managed_results (fn x => (case f x of NONE => () | some => raise FOUND some)) xs; |
43 in |
49 in |
44 (case get_first found results of |
50 (case get_first found results of |
45 SOME y => SOME y |
51 SOME y => SOME y |
46 | NONE => (Exn.release_first results; NONE)) |
52 | NONE => (Exn.release_first results; NONE)) |
47 end; |
53 end; |