# HG changeset patch
# User wenzelm
# Date 1689774992 -7200
# Node ID 092f1e435b3a6f8a23453b7dbed97faa84281d9c
# Parent  b262ecc983190dd1b31031e7436b46497436e855
proper Build_Cluster.Host.parse for parameters and system options;
clarified Build_Cluster.Host: empty "host" means local;

diff -r b262ecc98319 -r 092f1e435b3a src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Jul 19 15:40:02 2023 +0200
+++ b/src/Pure/Tools/build.scala	Wed Jul 19 15:56:32 2023 +0200
@@ -304,7 +304,7 @@
   Options are:
     -B NAME      include session NAME and all descendants
     -D DIR       include session directory and select its sessions
-    -H HOST      add host for distrubuted build
+    -H HOST      additional host for distributed build ("NAME:PARAMETERS")
     -N           cyclic shuffling of NUMA CPU nodes (performance tuning)
     -P DIR       enable HTML/PDF presentation in directory (":" for default)
     -R           refer to requirements of selected sessions
@@ -327,10 +327,14 @@
 
   Build and manage Isabelle sessions: ML heaps, session databases, documents.
 
+  Parameters for host specifications (option -H), apart from system options:
+""" + Library.indent_lines(4, Build_Cluster.Host.parameters.print()) +
+"""
+
   Notable system options: see "isabelle options -l -t build"
 
   Notable system settings:
-""" + Library.indent_lines(4,  Build_Log.Settings.show()) + "\n",
+""" + Library.indent_lines(4, Build_Log.Settings.show()) + "\n",
         "B:" -> (arg => base_sessions += arg),
         "D:" -> (arg => select_dirs += Path.explode(arg)),
         "H:" -> (arg => build_hosts += Build_Cluster.Host.parse(arg)),
diff -r b262ecc98319 -r 092f1e435b3a src/Pure/Tools/build_cluster.scala
--- a/src/Pure/Tools/build_cluster.scala	Wed Jul 19 15:40:02 2023 +0200
+++ b/src/Pure/Tools/build_cluster.scala	Wed Jul 19 15:56:32 2023 +0200
@@ -10,20 +10,61 @@
 
 object Build_Cluster {
   object Host {
-    val PORT = "port"
-    val JOBS = "jobs"
-    val NUMA = "numa"
+    private val rfc822_specials = """()<>@,;:\"[]"""
+
+    private val USER = "user"
+    private val PORT = "port"
+    private val JOBS = "jobs"
+    private val NUMA = "numa"
+
+    val parameters: Options =
+      Options.inline("""
+        option user : string = ""   -- "explicit SSH user"
+        option port : int = 0       -- "explicit SSH port"
+        option jobs : int = 1       -- "maximum number of parallel jobs"
+        option numa : bool = false  -- "cyclic shuffling of NUMA CPU nodes"
+      """)
+
+    def is_parameter(spec: Options.Spec): Boolean = parameters.defined(spec.name)
+
+    lazy val test_options: Options = Options.init0()
 
     def apply(
-      host: String,
-      user: String = "",
-      port: Int = 0,
-      jobs: Int = 1,
-      numa: Boolean = false,
+      host: String = "",
+      user: String = parameters.string(USER),
+      port: Int = parameters.int(PORT),
+      jobs: Int = parameters.int(JOBS),
+      numa: Boolean = parameters.bool(NUMA),
       options: List[Options.Spec] = Nil
     ): Host = new Host(host, user, port, jobs, numa, options)
 
-    def parse(str: String): Host = Host(host = str)  // FIXME proper parse
+    def parse(str: String): Host = {
+      val host = str.takeWhile(c => !rfc822_specials.contains(c))
+      val (params, options) =
+        try {
+          val rest = {
+            val n = str.length
+            val m = host.length
+            val l =
+              if (m == n) n
+              else if (str(m) == ':') m + 1
+              else error("Colon (:) expected after host name")
+            str.substring(l)
+          }
+          val (specs1, specs2) = Options.parse_specs(rest).partition(is_parameter)
+          (parameters ++ specs1, { test_options ++ specs2; specs2 })
+        }
+        catch {
+          case ERROR(msg) =>
+            cat_error(msg, "The error(s) above occurred in host specification " + quote(str))
+        }
+      apply(host = host,
+        user = params.string(USER),
+        port = params.int(PORT),
+        jobs = params.int(JOBS),
+        numa = params.bool(NUMA),
+        options = options)
+    }
   }
 
   final class Host private(
@@ -34,18 +75,21 @@
     numa: Boolean,
     options: List[Options.Spec]
   ) {
-    require(host.nonEmpty, "Undefined host name")
+    override def toString: String = print
 
-    override def toString: String = print
     def print: String = {
-      val props =
+      val params =
         List(
+          if (user.isEmpty) "" else Properties.Eq(Host.USER, user),
           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)
+      val rest = (params ::: options).mkString(",")
+
+      if (host.isEmpty) ":" + rest
+      else if (rest.isEmpty) host
+      else host + ":" + rest
     }
 
     def open_ssh_session(options: Options): SSH.Session =