--- a/src/Pure/Concurrent/future.ML Wed May 16 15:52:15 2018 +0200
+++ b/src/Pure/Concurrent/future.ML Wed May 16 21:06:28 2018 +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_finished: 'a future -> 'a
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
@@ -505,6 +506,8 @@
| exns => Exn.Exn (Par_Exn.make exns))
else res);
+fun get_finished x = Exn.release (get_result x);
+
local
fun join_next atts deps = (*requires SYNCHRONIZED*)