| changeset 72085 | 3afd6b1c7ab5 |
| parent 72084 | df99d26efeeb |
| child 72086 | 41e1e2395a67 |
--- a/src/Pure/Concurrent/future.ML Wed Aug 05 12:34:23 2020 +0200 +++ b/src/Pure/Concurrent/future.ML Wed Aug 05 12:42:43 2020 +0200 @@ -27,6 +27,7 @@ val default_params: params val forks: params -> (unit -> 'a) list -> 'a future list val fork: (unit -> 'a) -> 'a future + val get_result: 'a future -> 'a Exn.result val join_results: 'a future list -> 'a Exn.result list val join_result: 'a future -> 'a Exn.result val joins: 'a future list -> 'a list