# HG changeset patch
# User wenzelm
# Date 1708078362 -3600
# Node ID 0f01c575ff3ef037d5c961a1fc269b8270d4e9e3
# Parent  73b8ac4b0492b9aea800f33d73b16f847937ead2
clarified signature;

diff -r 73b8ac4b0492 -r 0f01c575ff3e src/Pure/Build/build_cluster.scala
--- a/src/Pure/Build/build_cluster.scala	Fri Feb 16 10:51:49 2024 +0100
+++ b/src/Pure/Build/build_cluster.scala	Fri Feb 16 11:12:42 2024 +0100
@@ -238,10 +238,10 @@
   def return_code(rc: Int): Unit = ()
   def return_code(res: Process_Result): Unit = return_code(res.rc)
   def return_code(exn: Throwable): Unit = return_code(Process_Result.RC(exn))
-  def open(): Unit = ()
-  def init(): Unit = ()
-  def benchmark(): Unit = ()
-  def start(): Unit = ()
+  def open(): Build_Cluster = this
+  def init(): Build_Cluster = this
+  def benchmark(): Build_Cluster = this
+  def start(): Build_Cluster = this
   def active(): Boolean = false
   def join: List[Build_Cluster.Result] = Nil
   def stop(): Unit = { join; close() }
@@ -284,7 +284,7 @@
 
   private var _sessions = List.empty[Build_Cluster.Session]
 
-  override def open(): Unit = synchronized {
+  override def open(): Build_Cluster = synchronized {
     require(_sessions.isEmpty, "build cluster already open")
 
     val attempts =
@@ -300,6 +300,8 @@
       for (case Exn.Res(session) <- attempts) session.close()
       error("Failed to connect build cluster")
     }
+
+    this
   }
 
 
@@ -307,7 +309,7 @@
 
   private var _init = List.empty[Future[Unit]]
 
-  override def init(): Unit = synchronized {
+  override def init(): Build_Cluster = synchronized {
     require(_sessions.nonEmpty, "build cluster not yet open")
 
     if (_init.isEmpty) {
@@ -319,9 +321,11 @@
           }
         }
     }
+
+    this
   }
   
-  override def benchmark(): Unit = synchronized {
+  override def benchmark(): Build_Cluster = synchronized {
     _init.foreach(_.join)
     _init =
       for (session <- _sessions if !session.host.shared) yield {
@@ -330,6 +334,8 @@
         }
       }
     _init.foreach(_.join)
+
+    this
   }
 
 
@@ -339,7 +345,7 @@
 
   override def active(): Boolean = synchronized { _workers.nonEmpty }
 
-  override def start(): Unit = synchronized {
+  override def start(): Build_Cluster = synchronized {
     require(_sessions.nonEmpty, "build cluster not yet open")
     require(_workers.isEmpty, "build cluster already active")
 
@@ -352,6 +358,8 @@
           Exn.release(capture(session.host, "work") { session.start() })
         }
       }
+
+    this
   }
 
   override def join: List[Build_Cluster.Result] = synchronized {
diff -r 73b8ac4b0492 -r 0f01c575ff3e src/Pure/Build/build_process.scala
--- a/src/Pure/Build/build_process.scala	Fri Feb 16 10:51:49 2024 +0100
+++ b/src/Pure/Build/build_process.scala	Fri Feb 16 11:12:42 2024 +0100
@@ -914,11 +914,8 @@
 
   protected val log: Logger = Logger.make_system_log(progress, build_options)
 
-  protected def open_build_cluster(): Build_Cluster = {
-    val build_cluster = Build_Cluster.make(build_context, progress = build_progress)
-    build_cluster.open()
-    build_cluster
-  }
+  protected def open_build_cluster(): Build_Cluster =
+    Build_Cluster.make(build_context, progress = build_progress).open()
 
   protected val _build_cluster =
     try {
diff -r 73b8ac4b0492 -r 0f01c575ff3e src/Pure/Build/build_schedule.scala
--- a/src/Pure/Build/build_schedule.scala	Fri Feb 16 10:51:49 2024 +0100
+++ b/src/Pure/Build/build_schedule.scala	Fri Feb 16 11:12:42 2024 +0100
@@ -1314,11 +1314,8 @@
       val hosts_current =
         cluster_hosts.forall(host => isabelle.Host.read_info(host_database, host.name).isDefined)
       if (!hosts_current) {
-        val build_cluster = Build_Cluster.make(build_context, progress = progress)
-        build_cluster.open()
-        build_cluster.init()
-        build_cluster.benchmark()
-        build_cluster.close()
+        Build_Cluster.make(build_context, progress = progress)
+          .open().init().benchmark().close()
       }
 
       val host_infos = Host_Infos.load(cluster_hosts, host_database)