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