--- a/etc/build.props Fri Nov 10 16:03:52 2023 +0100
+++ b/etc/build.props Sat Nov 11 13:31:14 2023 +0100
@@ -175,6 +175,7 @@
src/Pure/System/posix_interrupt.scala \
src/Pure/System/process_result.scala \
src/Pure/System/progress.scala \
+ src/Pure/System/registry.scala \
src/Pure/System/scala.scala \
src/Pure/System/system_channel.scala \
src/Pure/System/tty_loop.scala \
--- a/etc/settings Fri Nov 10 16:03:52 2023 +0100
+++ b/etc/settings Sat Nov 11 13:31:14 2023 +0100
@@ -138,6 +138,14 @@
###
+### Registry
+###
+
+isabelle_registry "$ISABELLE_HOME/etc/registry.toml?"
+isabelle_registry "$ISABELLE_HOME_USER/etc/registry.toml?"
+
+
+###
### Symbol rendering
###
--- a/lib/scripts/getfunctions Fri Nov 10 16:03:52 2023 +0100
+++ b/lib/scripts/getfunctions Sat Nov 11 13:31:14 2023 +0100
@@ -32,6 +32,22 @@
}
export -f tar
+#registry
+function isabelle_registry ()
+{
+ local X=""
+ for X in "$@"
+ do
+ if [ -z "$ISABELLE_REGISTRY" ]; then
+ ISABELLE_REGISTRY="$X"
+ elif [ -n "$X" ]; then
+ ISABELLE_REGISTRY="$ISABELLE_REGISTRY:$X"
+ fi
+ done
+ export ISABELLE_REGISTRY
+}
+export -f isabelle_registry
+
#OCaml management via OPAM
function isabelle_opam ()
{
--- a/src/Pure/General/toml.scala Fri Nov 10 16:03:52 2023 +0100
+++ b/src/Pure/General/toml.scala Sat Nov 11 13:31:14 2023 +0100
@@ -507,6 +507,11 @@
}
}
+ def parse_files(files: Iterable[Path], context: Parse_Context = Parse_Context()): Table = {
+ val s = files.iterator.map(File.read).mkString("\n\n")
+ parse(s, context = context)
+ }
+
/* Format TOML */
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/registry.scala Sat Nov 11 13:31:14 2023 +0100
@@ -0,0 +1,17 @@
+/* Title: Pure/System/registry.scala
+ Author: Makarius
+
+Hierarchic system configuration in TOML notation.
+*/
+
+package isabelle
+
+
+object Registry {
+ def files(): List[Path] =
+ Path.split_permissive_files(Isabelle_System.getenv("ISABELLE_REGISTRY"))
+
+ lazy val global: Registry = new Registry(TOML.parse_files(files()))
+}
+
+class Registry private(val toml: TOML.Table)
\ No newline at end of file