src/Pure/Concurrent/future.ML
changeset 44198 a41ea419de68
parent 44173 aaaa13e297dc
child 44247 270366301bd7
--- a/src/Pure/Concurrent/future.ML	Mon Aug 15 16:38:42 2011 +0200
+++ b/src/Pure/Concurrent/future.ML	Mon Aug 15 19:27:55 2011 +0200
@@ -39,6 +39,7 @@
   val task_of: 'a future -> Task_Queue.task
   val peek: 'a future -> 'a Exn.result option
   val is_finished: 'a future -> bool
+  val get_finished: 'a future -> 'a
   val interruptible_task: ('a -> 'b) -> 'a -> 'b
   val cancel_group: Task_Queue.group -> unit
   val cancel: 'a future -> unit
@@ -105,6 +106,11 @@
 fun peek x = Single_Assignment.peek (result_of x);
 fun is_finished x = is_some (peek x);
 
+fun get_finished x =
+  (case peek x of
+    SOME res => Exn.release res
+  | NONE => raise Fail "Unfinished future evaluation");
+
 
 
 (** scheduling **)