# HG changeset patch
# User wenzelm
# Date 1526497588 -7200
# Node ID 756434c77d218cf0e0402569fc01fdd8635fc770
# Parent  60795764005762a82cbbc79b6309c48f46c8ad26
tuned signature;

diff -r 607957640057 -r 756434c77d21 src/Pure/Concurrent/future.ML
--- 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*)