--- a/src/Pure/System/registry.scala Sat Nov 11 21:08:21 2023 +0100
+++ b/src/Pure/System/registry.scala Sat Nov 11 21:17:45 2023 +0100
@@ -8,11 +8,16 @@
object Registry {
+ /* registry files */
+
def files(): List[Path] =
Path.split_permissive_files(Isabelle_System.getenv("ISABELLE_REGISTRY"))
lazy val global: Registry = new Registry(TOML.parse_files(files()))
+
+ /* interpreted entries */
+
def err(msg: String, name: String): Nothing =
error(msg + " for registry entry " + quote(name))
@@ -32,6 +37,9 @@
}
}
+
+ /* build cluster resources */
+
object Host extends Table[List[Options.Spec]]("host") {
def options_spec(a: TOML.Key, b: TOML.T): Option[Options.Spec] =
TOML.Scalar.unapply(b).map(Options.Spec.eq(a, _))