src/Pure/Tools/build_cluster.scala
changeset 78413 6f3066a9b609
parent 78408 092f1e435b3a
child 78416 f26eba6281b1
--- a/src/Pure/Tools/build_cluster.scala	Thu Jul 20 11:10:28 2023 +0200
+++ b/src/Pure/Tools/build_cluster.scala	Thu Jul 20 12:02:52 2023 +0200
@@ -9,6 +9,8 @@
 
 
 object Build_Cluster {
+  /* host specifications */
+
   object Host {
     private val rfc822_specials = """()<>@,;:\"[]"""
 
@@ -75,6 +77,8 @@
     numa: Boolean,
     options: List[Options.Spec]
   ) {
+    def is_remote: Boolean = host.nonEmpty
+
     override def toString: String = print
 
     def print: String = {
@@ -95,4 +99,29 @@
     def open_ssh_session(options: Options): SSH.Session =
       SSH.open_session(options, host, port = port, user = user)
   }
+
+
+  /* remote sessions */
+
+  class Session(host: Host) extends AutoCloseable {
+    override def close(): Unit = ()
+  }
 }
+
+// class extensible via Build.Engine.build_process() and Build_Process.init_cluster()
+class Build_Cluster(
+  build_context: Build_Process.Context,
+  remote_hosts: List[Build_Cluster.Host],
+  progress: Progress = new Progress
+) extends AutoCloseable {
+  require(remote_hosts.nonEmpty && remote_hosts.forall(_.is_remote), "remote hosts required")
+
+  override def toString: String = remote_hosts.mkString("Build_Cluster(", ", ", ")")
+
+  progress.echo("Remote hosts:\n" + cat_lines(remote_hosts.map("  " + _)))
+
+  def start(): Unit = ()
+  def stop(): Unit = ()
+
+  override def close(): Unit = ()
+}