src/Pure/Concurrent/future.scala
changeset 38848 9483bb678d96
parent 34262 a6d2d9c07e46
child 45667 546d78f0d81f
--- a/src/Pure/Concurrent/future.scala	Sun Aug 29 18:55:48 2010 +0200
+++ b/src/Pure/Concurrent/future.scala	Sun Aug 29 19:04:29 2010 +0200
@@ -28,6 +28,7 @@
 {
   def peek: Option[Exn.Result[A]]
   def is_finished: Boolean = peek.isDefined
+  def get_finished: A = { require(is_finished); Exn.release(peek.get) }
   def join: A
   def map[B](f: A => B): Future[B] = Future.fork { f(join) }