# HG changeset patch
# User wenzelm
# Date 1699730003 -3600
# Node ID 73162a487f94d56daa352eb246cb3a8736081f24
# Parent  b0b86fead48cef0478e6be917745c934c63b2274
build cluster host specifications are based on registry entries (table prefix "host");

diff -r b0b86fead48c -r 73162a487f94 src/Pure/System/registry.scala
--- a/src/Pure/System/registry.scala	Sat Nov 11 20:08:20 2023 +0100
+++ b/src/Pure/System/registry.scala	Sat Nov 11 20:13:23 2023 +0100
@@ -31,6 +31,14 @@
         case _ => err("Table expected", Long_Name.qualify(prefix, name))
       }
   }
+
+  object Host extends Table[List[Options.Spec]]("host") {
+    def options_spec(a: TOML.Key, b: TOML.T): Option[Options.Spec] =
+      TOML.Scalar.unapply(b).map(Options.Spec.eq(a, _, permissive = true))
+
+    override def table_value(a: String, t: TOML.Table): List[Options.Spec] =
+      for ((a, b) <- t.any.values; s <- options_spec(a, b)) yield s
+  }
 }
 
 class Registry private(val table: TOML.Table) {
diff -r b0b86fead48c -r 73162a487f94 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sat Nov 11 20:08:20 2023 +0100
+++ b/src/Pure/Tools/build.scala	Sat Nov 11 20:13:23 2023 +0100
@@ -377,7 +377,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(Registry.global, arg)),
         "N" -> (_ => numa_shuffling = true),
         "P:" -> (arg => browser_info = Browser_Info.Config.make(arg)),
         "R" -> (_ => requirements = true),
diff -r b0b86fead48c -r 73162a487f94 src/Pure/Tools/build_cluster.scala
--- a/src/Pure/Tools/build_cluster.scala	Sat Nov 11 20:08:20 2023 +0100
+++ b/src/Pure/Tools/build_cluster.scala	Sat Nov 11 20:13:23 2023 +0100
@@ -56,27 +56,32 @@
       new Host(name, hostname, user, port, jobs, numa, dirs, shared, options)
     }
 
-    def parse(str: String): List[Host] = {
+    def parse(registry: Registry, str: String): List[Host] = {
+      def err(msg: String): Nothing =
+        cat_error(msg, "The error(s) above occurred in host specification " + quote(str))
+
       val names = str.takeWhile(c => !rfc822_specials.contains(c) || c == ',')
-      val (params, options) =
+      val more_specs =
         try {
-          val rest = {
-            val n = str.length
-            val m = names.length
-            val l =
-              if (m == n) n
-              else if (str(m) == ':') m + 1
-              else error("Missing \":\" after host name")
-            str.substring(l)
+          val n = str.length
+          val m = names.length
+          val l =
+            if (m == n) n
+            else if (str(m) == ':') m + 1
+            else error("Missing \":\" after host name")
+          Options.Spec.parse(str.substring(l))
+        }
+        catch { case ERROR(msg) => err(msg) }
+
+      for (name <- space_explode(',', names)) yield {
+        val base_specs = registry.get(Registry.Host, name)
+        val (params, options) =
+          try {
+            val (specs1, specs2) = (base_specs ::: more_specs).partition(is_parameter)
+            (parameters ++ specs1, { test_options ++ specs2; specs2 })
           }
-          val (specs1, specs2) = Options.Spec.parse(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))
-        }
-      for (name <- space_explode(',', names)) yield {
+          catch { case ERROR(msg) => err(msg) }
+
         apply(name = name,
           hostname = params.string(HOSTNAME),
           user = params.string(USER),
@@ -89,8 +94,8 @@
       }
     }
 
-    def parse_single(str: String): Host =
-      Library.the_single(parse(str), "Single host expected: " + quote(str))
+    def parse_single(registry: Registry, str: String): Host =
+      Library.the_single(parse(registry, str), "Single host expected: " + quote(str))
   }
 
   class Host(