# HG changeset patch
# User wenzelm
# Date 1699823892 -3600
# Node ID a2de1f6ff94e36c3f0381630e2df5a2cbfc9289e
# Parent  30360ee939f4ae552e93a614984d7292d5e9f577
support for "cluster" table with "hosts" array, and params/options as for "host" table;
support for "isabelle build -H cluster.name";

diff -r 30360ee939f4 -r a2de1f6ff94e src/Pure/System/registry.scala
--- a/src/Pure/System/registry.scala	Sun Nov 12 22:05:59 2023 +0100
+++ b/src/Pure/System/registry.scala	Sun Nov 12 22:18:12 2023 +0100
@@ -74,6 +74,23 @@
   }
   object Host extends Host
   object Host_Strict extends Host with Strict
+  object Host_Cluster extends Host with Strict { override def prefix = Cluster.prefix }
+
+  object Cluster extends Table with Strict {
+    def prefix = "cluster"
+    def prefix_hosts = "hosts"
+    type A = List[(String, List[Options.Spec])]
+
+    override def table_value(registry: Registry, t: TOML.Table, a: String): A = {
+      val hosts =
+        t.array.get(prefix_hosts) match {
+          case Some(arr) => arr.string.values.map(_.rep)
+          case None => bad_value(Long_Name.qualify(a, prefix_hosts))
+        }
+      val cluster_specs = Host_Cluster.get(registry, a)
+      hosts.map(h => (h, Host_Strict.get(registry, h) ::: cluster_specs))
+    }
+  }
 }
 
 class Registry private(val root: TOML.Table) {
diff -r 30360ee939f4 -r a2de1f6ff94e src/Pure/Tools/build_cluster.scala
--- a/src/Pure/Tools/build_cluster.scala	Sun Nov 12 22:05:59 2023 +0100
+++ b/src/Pure/Tools/build_cluster.scala	Sun Nov 12 22:18:12 2023 +0100
@@ -73,16 +73,22 @@
         }
         catch { case ERROR(msg) => err(msg) }
 
-      for (name <- space_explode(',', names)) yield {
-        val base_specs = Registry.Host.get(registry, name)
+      def get_registry(a: String): Registry.Cluster.A =
+        Registry.Cluster.try_unqualify(a) match {
+          case Some(b) => Registry.Cluster.get(registry, b)
+          case None => List(a -> Registry.Host.get(registry, a))
+        }
+
+      for (name <- space_explode(',', names); (host, host_specs) <- get_registry(name))
+      yield {
         val (params, options) =
           try {
-            val (specs1, specs2) = (base_specs ::: more_specs).partition(is_parameter)
+            val (specs1, specs2) = (host_specs ::: more_specs).partition(is_parameter)
             (parameters ++ specs1, { test_options ++ specs2; specs2 })
           }
           catch { case ERROR(msg) => err(msg) }
 
-        apply(name = name,
+        apply(name = host,
           hostname = params.string(HOSTNAME),
           user = params.string(USER),
           port = params.int(PORT),