# HG changeset patch
# User wenzelm
# Date 1689707171 -7200
# Node ID facf1a324807712e6f55e08a5a25cb2d5241e640
# Parent  ea5adf7acc2d9cd78fe00c041be8d158c1bb4792
more operations;

diff -r ea5adf7acc2d -r facf1a324807 src/Pure/Tools/build_cluster.scala
--- a/src/Pure/Tools/build_cluster.scala	Tue Jul 18 20:14:57 2023 +0200
+++ b/src/Pure/Tools/build_cluster.scala	Tue Jul 18 21:06:11 2023 +0200
@@ -9,4 +9,44 @@
 
 
 object Build_Cluster {
+  object Host {
+    val PORT = "port"
+    val JOBS = "jobs"
+    val NUMA = "numa"
+
+    def apply(
+      host: String,
+      user: String = "",
+      port: Int = 0,
+      jobs: Int = 1,
+      numa: Boolean = false,
+      options: List[Options.Spec] = Nil
+    ): Host = new Host(host, user, port, jobs, numa, options)
+  }
+
+  final class Host private(
+    host: String,
+    user: String,
+    port: Int,
+    jobs: Int,
+    numa: Boolean,
+    options: List[Options.Spec]
+  ) {
+    require(host.nonEmpty, "Undefined host name")
+
+    override def toString: String = print
+    def print: String = {
+      val props =
+        List(
+          if (port == 0) "" else Properties.Eq(Host.PORT, port.toString),
+          if (jobs == 1) "" else Properties.Eq(Host.JOBS, jobs.toString),
+          if_proper(numa, Host.NUMA)
+        ).filter(_.nonEmpty)
+      val rest = (props ::: options).mkString(",")
+      if_proper(user, user + "@") + host + if_proper(rest, ":" + rest)
+    }
+
+    def open_ssh_session(options: Options): SSH.Session =
+      SSH.open_session(options, host, port = port, user = user)
+  }
 }