tuned signature;
authorwenzelm
Wed May 16 21:06:28 2018 +0200 (12 months ago)
changeset 68196756434c77d21
parent 68195 607957640057
child 68197 7857817403e4
tuned signature;
src/Pure/Concurrent/future.ML
     1.1 --- a/src/Pure/Concurrent/future.ML	Wed May 16 15:52:15 2018 +0200
     1.2 +++ b/src/Pure/Concurrent/future.ML	Wed May 16 21:06:28 2018 +0200
     1.3 @@ -27,6 +27,7 @@
     1.4    val default_params: params
     1.5    val forks: params -> (unit -> 'a) list -> 'a future list
     1.6    val fork: (unit -> 'a) -> 'a future
     1.7 +  val get_finished: 'a future -> 'a
     1.8    val join_results: 'a future list -> 'a Exn.result list
     1.9    val join_result: 'a future -> 'a Exn.result
    1.10    val joins: 'a future list -> 'a list
    1.11 @@ -505,6 +506,8 @@
    1.12          | exns => Exn.Exn (Par_Exn.make exns))
    1.13        else res);
    1.14  
    1.15 +fun get_finished x = Exn.release (get_result x);
    1.16 +
    1.17  local
    1.18  
    1.19  fun join_next atts deps = (*requires SYNCHRONIZED*)