# 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) + } }