# HG changeset patch # User wenzelm # Date 1699815525 -3600 # Node ID f4e7dec70fa45c0e837ab33ba5a875ccde2b374a # Parent 78698a97afb36148e667432559b23e54ac2bf70c clarified signature; diff -r 78698a97afb3 -r f4e7dec70fa4 src/Pure/System/registry.scala --- 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) } } }