# HG changeset patch
# User wenzelm
# Date 1699816791 -3600
# Node ID 11045cf2b5c2c3584e2b10f5bf665a913155a8db
# Parent  f4e7dec70fa45c0e837ab33ba5a875ccde2b374a
tuned signature: more operations;

diff -r f4e7dec70fa4 -r 11045cf2b5c2 src/Pure/General/long_name.scala
--- a/src/Pure/General/long_name.scala	Sun Nov 12 19:58:45 2023 +0100
+++ b/src/Pure/General/long_name.scala	Sun Nov 12 20:19:51 2023 +0100
@@ -27,4 +27,12 @@
   def base_name(name: String): String =
     if (name == "") ""
     else explode(name).last
+
+  def try_unqualify(qual: String, name: String): Option[String] = {
+    val m = qual.length
+    val n = name.length
+    if (0 < m && m < n && name.startsWith(qual) && name(m) == separator_char)
+      Some(name.substring(m + 1))
+    else None
+  }
 }
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
   }