src/Pure/Concurrent/future.scala
changeset 71685 d5773922358d
parent 64370 865b39487b5d
child 71690 fef74c06cfac
equal deleted inserted replaced
71684:5036edb025b7 71685:d5773922358d
   133 
   133 
   134 private class Thread_Future[A](name: String, daemon: Boolean, body: => A) extends Future[A]
   134 private class Thread_Future[A](name: String, daemon: Boolean, body: => A) extends Future[A]
   135 {
   135 {
   136   private val result = Future.promise[A]
   136   private val result = Future.promise[A]
   137   private val thread =
   137   private val thread =
   138     Standard_Thread.fork(name, daemon) { result.fulfill_result(Exn.capture(body)) }
   138     Standard_Thread.fork(name = name, daemon = daemon) { result.fulfill_result(Exn.capture(body)) }
   139 
   139 
   140   def peek: Option[Exn.Result[A]] = result.peek
   140   def peek: Option[Exn.Result[A]] = result.peek
   141   def join_result: Exn.Result[A] = result.join_result
   141   def join_result: Exn.Result[A] = result.join_result
   142   def cancel: Unit = thread.interrupt
   142   def cancel: Unit = thread.interrupt
   143 }
   143 }