# HG changeset patch
# User wenzelm
# Date 1699824843 -3600
# Node ID 890783dc4bc63c932d167b02dc3fe56c5d823822
# Parent  a2de1f6ff94e36c3f0381630e2df5a2cbfc9289e
tuned signature;

diff -r a2de1f6ff94e -r 890783dc4bc6 src/Pure/System/registry.scala
--- a/src/Pure/System/registry.scala	Sun Nov 12 22:18:12 2023 +0100
+++ b/src/Pure/System/registry.scala	Sun Nov 12 22:34:03 2023 +0100
@@ -26,12 +26,12 @@
     def qualify(name: String): String = Long_Name.qualify(prefix, name)
     def try_unqualify(name: String): Option[String] = Long_Name.try_unqualify(prefix, name)
 
-    type A
+    type Value
     def bad_value(name: String): Nothing = error("Bad registry entry " + quote(qualify(name)))
-    def default_value(registry: Registry, name: String): A
-    def value(registry: Registry, t: TOML.T, name: String): A
+    def default_value(registry: Registry, name: String): Value
+    def value(registry: Registry, t: TOML.T, name: String): Value
 
-    def get(registry: Registry, name: String): A = {
+    def get(registry: Registry, name: String): Value = {
       registry.root.any.get(prefix) match {
         case None => default_value(registry, name)
         case Some(t: TOML.Table) =>
@@ -45,14 +45,14 @@
   }
 
   trait Strict extends Category {
-    override def default_value(registry: Registry, name: String): A = bad_value(name)
+    override def default_value(registry: Registry, name: String): Value = bad_value(name)
   }
 
   trait Table extends Category {
-    def table_value(registry: Registry, table: TOML.Table, name: String): A
-    override def default_value(registry: Registry, name: String): A =
+    def table_value(registry: Registry, table: TOML.Table, name: String): Value
+    override def default_value(registry: Registry, name: String): Value =
       table_value(registry, TOML.Table.empty, name)
-    override def value(registry: Registry, t: TOML.T, name: String): A =
+    override def value(registry: Registry, t: TOML.T, name: String): Value =
       t match {
         case table: TOML.Table => table_value(registry, table, name)
         case _ => bad_value(name)
@@ -64,12 +64,12 @@
 
   trait Host extends Table {
     def prefix = "host"
-    type A = List[Options.Spec]
+    type Value = List[Options.Spec]
 
     def options_spec(a: TOML.Key, b: TOML.T): Option[Options.Spec] =
       TOML.Scalar.unapply(b).map(Options.Spec.eq(a, _))
 
-    override def table_value(registry: Registry, t: TOML.Table, a: String): A =
+    override def table_value(registry: Registry, t: TOML.Table, a: String): Value =
       for ((a, b) <- t.any.values; s <- options_spec(a, b)) yield s
   }
   object Host extends Host
@@ -79,9 +79,9 @@
   object Cluster extends Table with Strict {
     def prefix = "cluster"
     def prefix_hosts = "hosts"
-    type A = List[(String, List[Options.Spec])]
+    type Value = List[(String, List[Options.Spec])]
 
-    override def table_value(registry: Registry, t: TOML.Table, a: String): A = {
+    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)
diff -r a2de1f6ff94e -r 890783dc4bc6 src/Pure/Tools/build_cluster.scala
--- a/src/Pure/Tools/build_cluster.scala	Sun Nov 12 22:18:12 2023 +0100
+++ b/src/Pure/Tools/build_cluster.scala	Sun Nov 12 22:34:03 2023 +0100
@@ -73,7 +73,7 @@
         }
         catch { case ERROR(msg) => err(msg) }
 
-      def get_registry(a: String): Registry.Cluster.A =
+      def get_registry(a: String): Registry.Cluster.Value =
         Registry.Cluster.try_unqualify(a) match {
           case Some(b) => Registry.Cluster.get(registry, b)
           case None => List(a -> Registry.Host.get(registry, a))