# 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) + } + } }