diff -r f4e7dec70fa4 -r 11045cf2b5c2 src/Pure/System/registry.scala --- a/src/Pure/System/registry.scala Sun Nov 12 19:58:45 2023 +0100 +++ b/src/Pure/System/registry.scala Sun Nov 12 20:19:51 2023 +0100 @@ -22,8 +22,11 @@ abstract class Category[A](val prefix: String) { override def toString: String = "Registry.Category(" + quote(prefix) + ")" + def qualify(name: String): String = Long_Name.qualify(prefix, name) + def try_unqualify(name: String): Option[String] = Long_Name.try_unqualify(prefix, name) + def bad_value(name: String): Nothing = - error("Bad registry entry " + quote(Long_Name.qualify(prefix, name))) + error("Bad registry entry " + quote(qualify(name))) def default_value(name: String): A def value(name: String, t: TOML.T): A }