export Par_List.managed_results, to enable specific treatment of results apart from default Par_Exn.release_first;
1.1 --- a/src/Pure/Concurrent/par_list.ML Thu Aug 18 15:15:43 2011 +0200
1.2 +++ b/src/Pure/Concurrent/par_list.ML Thu Aug 18 15:37:01 2011 +0200
1.3 @@ -16,6 +16,7 @@
1.4
1.5 signature PAR_LIST =
1.6 sig
1.7 + val managed_results: string -> ('a -> 'b) -> 'a list -> 'b Exn.result list
1.8 val map_name: string -> ('a -> 'b) -> 'a list -> 'b list
1.9 val map: ('a -> 'b) -> 'a list -> 'b list
1.10 val get_some: ('a -> 'b option) -> 'a list -> 'b option