# HG changeset patch
# User wenzelm
# Date 1699727819 -3600
# Node ID 409442cb781436a0d1b9e2ad7e630ae292049e9e
# Parent  bc7b7357f4bc49136638630cd13e6d838ef6f379
support interpreted/typed entries via Registry.Category and Registry.Table;

diff -r bc7b7357f4bc -r 409442cb7814 src/Pure/System/registry.scala
--- a/src/Pure/System/registry.scala	Sat Nov 11 18:39:57 2023 +0100
+++ b/src/Pure/System/registry.scala	Sat Nov 11 19:36:59 2023 +0100
@@ -12,8 +12,39 @@
     Path.split_permissive_files(Isabelle_System.getenv("ISABELLE_REGISTRY"))
 
   lazy val global: Registry = new Registry(TOML.parse_files(files()))
+
+  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 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 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))
+      }
+  }
 }
 
-class Registry private(val toml: TOML.Table) {
-  override def toString: String = TOML.Format(toml)
+class Registry private(val table: TOML.Table) {
+  override def toString: String = TOML.Format(table)
+
+  def get[A](category: Registry.Category[A], name: String): A = {
+    table.any.get(category.prefix) match {
+      case None => category.default_value
+      case Some(t: TOML.Table) =>
+        t.any.get(name) match {
+          case None => category.default_value
+          case Some(u) => category.value(name, u)
+        }
+      case Some(_) => Registry.err("Table expected", category.prefix)
+    }
+  }
 }