support multiple host names;

--- a/src/Pure/Tools/build.scala	Fri Aug 25 15:31:14 2023 +0200
+++ b/src/Pure/Tools/build.scala	Fri Aug 25 20:08:32 2023 +0200
@@ -345,7 +345,8 @@
     -A ROOT      include AFP with given root directory (":" for """ + AFP.BASE.implode + """)
     -B NAME      include session NAME and all descendants
     -D DIR       include session directory and select its sessions
-    -H HOST      additional host for distributed build ("NAME:PARAMETERS")
+    -H HOSTS     additional build cluster host specifications, of the form
+                 "NAMES:PARAMETERS" (separated by commas)
     -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
@@ -379,7 +380,7 @@
         "A:" -> (arg => afp_root = Some(if (arg == ":") AFP.BASE else Path.explode(arg))),
         "B:" -> (arg => base_sessions += arg),
         "D:" -> (arg => select_dirs += Path.explode(arg)),
-        "H:" -> (arg => build_hosts += Build_Cluster.Host.parse(arg)),
+        "H:" -> (arg => build_hosts ++= Build_Cluster.Host.parse(arg)),
         "N" -> (_ => numa_shuffling = true),
         "P:" -> (arg => browser_info = Browser_Info.Config.make(arg)),
         "R" -> (_ => requirements = true),

--- a/src/Pure/Tools/build_cluster.scala	Fri Aug 25 15:31:14 2023 +0200
+++ b/src/Pure/Tools/build_cluster.scala	Fri Aug 25 20:08:32 2023 +0200
@@ -47,13 +47,13 @@
       options: List[Options.Spec] = Nil
     ): Host = new Host(name, user, port, jobs, numa, shared, options)
 
-    def parse(str: String): Host = {
-      val name = str.takeWhile(c => !rfc822_specials.contains(c))
+    def parse(str: String): List[Host] = {
+      val names = str.takeWhile(c => !rfc822_specials.contains(c) || c == ',')
       val (params, options) =
         try {
           val rest = {
             val n = str.length
-            val m = name.length
+            val m = names.length
             val l =
               if (m == n) n
               else if (str(m) == ':') m + 1
@@ -67,13 +67,15 @@
           case ERROR(msg) =>
             cat_error(msg, "The error(s) above occurred in host specification " + quote(str))
         }
-      apply(name = name,
-        user = params.string(USER),
-        port = params.int(PORT),
-        jobs = params.int(JOBS),
-        numa = params.bool(NUMA),
-        shared = params.bool(SHARED),
-        options = options)
+      for (name <- space_explode(',', names)) yield {
+        apply(name = name,
+          user = params.string(USER),
+          port = params.int(PORT),
+          jobs = params.int(JOBS),
+          numa = params.bool(NUMA),
+          shared = params.bool(SHARED),
+          options = options)
+      }
     }
   }