--- a/src/Pure/System/registry.scala Sun Nov 12 12:54:26 2023 +0100
+++ b/src/Pure/System/registry.scala Sun Nov 12 19:58:45 2023 +0100
@@ -20,22 +20,21 @@
/* interpreted entries */
- def err(msg: String, name: String): Nothing =
- error(msg + " for registry entry " + quote(name))
-
abstract class Category[A](val prefix: String) {
override def toString: String = "Registry.Category(" + quote(prefix) + ")"
- def default_value: A
+ def bad_value(name: String): Nothing =
+ error("Bad registry entry " + quote(Long_Name.qualify(prefix, name)))
+ def default_value(name: String): A
def value(name: String, t: TOML.T): A
}
abstract class Table[A](prefix: String) extends Category[A](prefix) {
def table_value(name: String, table: TOML.Table): A
- override def default_value: A = table_value("", TOML.Table.empty)
+ override def default_value(name: String): A = table_value(name, TOML.Table.empty)
override def value(name: String, t: TOML.T): A =
t match {
case table: TOML.Table => table_value(name, table)
- case _ => err("Table expected", Long_Name.qualify(prefix, name))
+ case _ => bad_value(name)
}
}
@@ -65,13 +64,13 @@
def get[A](category: Registry.Category[A], name: String): A = {
table.any.get(category.prefix) match {
- case None => category.default_value
+ case None => category.default_value(name)
case Some(t: TOML.Table) =>
t.any.get(name) match {
- case None => category.default_value
+ case None => category.default_value(name)
case Some(u) => category.value(name, u)
}
- case Some(_) => Registry.err("Table expected", category.prefix)
+ case Some(_) => category.bad_value(name)
}
}
}