--- a/src/Pure/Concurrent/future.scala Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Pure/Concurrent/future.scala Thu Mar 04 21:04:27 2021 +0100
@@ -38,7 +38,7 @@
def join_result: Exn.Result[A]
def join: A = Exn.release(join_result)
def map[B](f: A => B): Future[B] = Future.fork { f(join) }
- def cancel: Unit
+ def cancel(): Unit
override def toString: String =
peek match {
@@ -61,7 +61,7 @@
{
val peek: Option[Exn.Result[A]] = Some(Exn.Res(x))
def join_result: Exn.Result[A] = peek.get
- def cancel: Unit = {}
+ def cancel(): Unit = {}
}
@@ -93,7 +93,7 @@
if (do_run) {
val result = Exn.capture(body)
status.change(_ => Terminated)
- status.change(_ => Finished(if (Thread.interrupted) Exn.Exn(Exn.Interrupt()) else result))
+ status.change(_ => Finished(if (Thread.interrupted()) Exn.Exn(Exn.Interrupt()) else result))
}
}
private val task = Isabelle_Thread.pool.submit(new Callable[Unit] { def call = try_run() })
@@ -107,11 +107,11 @@
}
}
- def cancel =
+ def cancel(): Unit =
{
status.change {
case Ready => task.cancel(false); Finished(Exn.Exn(Exn.Interrupt()))
- case st @ Running(thread) => thread.interrupt; st
+ case st @ Running(thread) => thread.interrupt(); st
case st => st
}
}
@@ -133,7 +133,7 @@
def fulfill(x: A): Unit = fulfill_result(Exn.Res(x))
- def cancel: Unit =
+ def cancel(): Unit =
state.change(st => if (st.isEmpty) Some(Exn.Exn(Exn.Interrupt())) else st)
}
@@ -157,5 +157,5 @@
def peek: Option[Exn.Result[A]] = result.peek
def join_result: Exn.Result[A] = result.join_result
- def cancel: Unit = thread.interrupt
+ def cancel(): Unit = thread.interrupt()
}