--- 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 **)