src/Pure/System/registry.scala
changeset 78961 11045cf2b5c2
parent 78960 f4e7dec70fa4
child 78962 7a58c1199de3
--- 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
   }