equal
deleted
inserted
replaced
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 } |