src/Pure/Concurrent/future.scala

--- a/src/Pure/Concurrent/future.scala	Fri Apr 01 11:51:42 2022 +0200
+++ b/src/Pure/Concurrent/future.scala	Fri Apr 01 17:06:10 2022 +0200
@@ -12,8 +12,7 @@
 
 /* futures and promises */
 
-object Future
-{
+object Future {
   def value[A](x: A): Future[A] = new Value_Future(x)
   def fork[A](body: => A): Future[A] = new Task_Future[A](body)
   def promise[A]: Promise[A] = new Promise_Future[A]
@@ -24,14 +23,14 @@
     pri: Int = Thread.NORM_PRIORITY,
     daemon: Boolean = false,
     inherit_locals: Boolean = false,
-    uninterruptible: Boolean = false)(body: => A): Future[A] =
-    {
-      new Thread_Future[A](name, group, pri, daemon, inherit_locals, uninterruptible, body)
-    }
+    uninterruptible: Boolean = false)(
+    body: => A
+  ): Future[A] = {
+    new Thread_Future[A](name, group, pri, daemon, inherit_locals, uninterruptible, body)
+  }
 }
 
-trait Future[A]
-{
+trait Future[A] {
   def peek: Option[Exn.Result[A]]
   def is_finished: Boolean = peek.isDefined
   def get_finished: A = { require(is_finished, "future not finished"); Exn.release(peek.get) }
@@ -48,8 +47,7 @@
     }
 }
 
-trait Promise[A] extends Future[A]
-{
+trait Promise[A] extends Future[A] {
   def fulfill_result(res: Exn.Result[A]): Unit
   def fulfill(x: A): Unit
 }
@@ -57,8 +55,7 @@
 
 /* value future */
 
-private class Value_Future[A](x: A) extends Future[A]
-{
+private class Value_Future[A](x: A) extends Future[A] {
   val peek: Option[Exn.Result[A]] = Some(Exn.Res(x))
   def join_result: Exn.Result[A] = peek.get
   def cancel(): Unit = {}
@@ -67,8 +64,7 @@
 
 /* task future via thread pool */
 
-private class Task_Future[A](body: => A) extends Future[A]
-{
+private class Task_Future[A](body: => A) extends Future[A] {
   private sealed abstract class Status
   private case object Ready extends Status
   private case class Running(thread: Thread) extends Status
@@ -83,8 +79,7 @@
       case _ => None
     }
 
-  private def try_run(): Unit =
-  {
+  private def try_run(): Unit = {
     val do_run =
       status.change_result {
         case Ready => (true, Running(Thread.currentThread))
@@ -98,8 +93,7 @@
   }
   private val task = Isabelle_Thread.pool.submit(new Callable[Unit] { def call = try_run() })
 
-  def join_result: Exn.Result[A] =
-  {
+  def join_result: Exn.Result[A] = {
     try_run()
     status.guarded_access {
       case st @ Finished(result) => Some((result, st))
@@ -107,8 +101,7 @@
     }
   }
 
-  def cancel(): Unit =
-  {
+  def cancel(): Unit = {
     status.change {
       case Ready => task.cancel(false); Finished(Exn.Exn(Exn.Interrupt()))
       case st @ Running(thread) => thread.interrupt(); st
@@ -120,8 +113,7 @@
 
 /* promise future */
 
-private class Promise_Future[A] extends Promise[A]
-{
+private class Promise_Future[A] extends Promise[A] {
   private val state = Synchronized[Option[Exn.Result[A]]](None)
   def peek: Option[Exn.Result[A]] = state.value
 
@@ -147,13 +139,12 @@
   daemon: Boolean,
   inherit_locals: Boolean,
   uninterruptible: Boolean,
-  body: => A) extends Future[A]
-{
+  body: => A) extends Future[A] {
   private val result = Future.promise[A]
   private val thread =
     Isabelle_Thread.fork(name = name, group = group, pri = pri, daemon = daemon,
-      inherit_locals = inherit_locals, uninterruptible = uninterruptible)
-    { result.fulfill_result(Exn.capture(body)) }
+      inherit_locals = inherit_locals, uninterruptible = uninterruptible) {
+      result.fulfill_result(Exn.capture(body)) }
 
   def peek: Option[Exn.Result[A]] = result.peek
   def join_result: Exn.Result[A] = result.join_result