clarified signature;
authorwenzelm
Sun, 12 Nov 2023 19:58:45 +0100
changeset 78960 f4e7dec70fa4
parent 78959 78698a97afb3
child 78961 11045cf2b5c2
clarified signature;
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)
     }
   }
 }