more robust: disallow empty clusters, so "isabelle build -H" really means cluster build;
authorwenzelm
Sat, 17 Feb 2024 17:33:27 +0100
changeset 79651 155bb0ae4ae2
parent 79650 65ef68bab8d6
child 79652 93e6ca9e7595
more robust: disallow empty clusters, so "isabelle build -H" really means cluster build;
src/Pure/System/registry.scala
--- a/src/Pure/System/registry.scala	Sat Feb 17 17:23:22 2024 +0100
+++ b/src/Pure/System/registry.scala	Sat Feb 17 17:33:27 2024 +0100
@@ -84,8 +84,8 @@
     override def table_value(registry: Registry, t: TOML.Table, a: String): Value = {
       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))
+          case Some(arr) if arr.length > 0 => arr.string.values.map(_.rep)
+          case _ => 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))