equal
deleted
inserted
replaced
44 Future.forks {name = name, group = SOME group, deps = [], pri = pri, interrupts = true} |
44 Future.forks {name = name, group = SOME group, deps = [], pri = pri, interrupts = true} |
45 (map (fn x => fn () => f x) xs); |
45 (map (fn x => fn () => f x) xs); |
46 val results = |
46 val results = |
47 restore_attributes Future.join_results futures |
47 restore_attributes Future.join_results futures |
48 handle exn => |
48 handle exn => |
49 (if Exn.is_interrupt exn then Future.cancel_group group else (); reraise exn); |
49 (if Exn.is_interrupt exn then Future.cancel_group group else (); Exn.reraise exn); |
50 in results end) (); |
50 in results end) (); |
51 |
51 |
52 fun map_name name f xs = Par_Exn.release_first (managed_results name f xs); |
52 fun map_name name f xs = Par_Exn.release_first (managed_results name f xs); |
53 fun map f = map_name "Par_List.map" f; |
53 fun map f = map_name "Par_List.map" f; |
54 fun map_independent f = map (Exn.interruptible_capture f) #> Par_Exn.release_all; |
54 fun map_independent f = map (Exn.interruptible_capture f) #> Par_Exn.release_all; |