author | wenzelm |
Sat, 11 Nov 2023 21:17:45 +0100 | |
changeset 78950 | cd350dcd912a |
parent 78947 | 2a27d2c8eae8 |
child 78951 | c8c40e11c907 |
permissions | -rw-r--r-- |
78939 | 1 |
/* Title: Pure/System/registry.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Hierarchic system configuration in TOML notation. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
10 |
object Registry { |
|
78950 | 11 |
/* registry files */ |
12 |
||
78939 | 13 |
def files(): List[Path] = |
14 |
Path.split_permissive_files(Isabelle_System.getenv("ISABELLE_REGISTRY")) |
|
15 |
||
16 |
lazy val global: Registry = new Registry(TOML.parse_files(files())) |
|
78942
409442cb7814
support interpreted/typed entries via Registry.Category and Registry.Table;
wenzelm
parents:
78940
diff
changeset
|
17 |
|
78950 | 18 |
|
19 |
/* interpreted entries */ |
|
20 |
||
78942
409442cb7814
support interpreted/typed entries via Registry.Category and Registry.Table;
wenzelm
parents:
78940
diff
changeset
|
21 |
def err(msg: String, name: String): Nothing = |
409442cb7814
support interpreted/typed entries via Registry.Category and Registry.Table;
wenzelm
parents:
78940
diff
changeset
|
22 |
error(msg + " for registry entry " + quote(name)) |
409442cb7814
support interpreted/typed entries via Registry.Category and Registry.Table;
wenzelm
parents:
78940
diff
changeset
|
23 |
|
409442cb7814
support interpreted/typed entries via Registry.Category and Registry.Table;
wenzelm
parents:
78940
diff
changeset
|
24 |
abstract class Category[A](val prefix: String) { |
409442cb7814
support interpreted/typed entries via Registry.Category and Registry.Table;
wenzelm
parents:
78940
diff
changeset
|
25 |
override def toString: String = "Registry.Category(" + quote(prefix) + ")" |
409442cb7814
support interpreted/typed entries via Registry.Category and Registry.Table;
wenzelm
parents:
78940
diff
changeset
|
26 |
def default_value: A |
409442cb7814
support interpreted/typed entries via Registry.Category and Registry.Table;
wenzelm
parents:
78940
diff
changeset
|
27 |
def value(name: String, t: TOML.T): A |
409442cb7814
support interpreted/typed entries via Registry.Category and Registry.Table;
wenzelm
parents:
78940
diff
changeset
|
28 |
} |
409442cb7814
support interpreted/typed entries via Registry.Category and Registry.Table;
wenzelm
parents:
78940
diff
changeset
|
29 |
|
409442cb7814
support interpreted/typed entries via Registry.Category and Registry.Table;
wenzelm
parents:
78940
diff
changeset
|
30 |
abstract class Table[A](prefix: String) extends Category[A](prefix) { |
409442cb7814
support interpreted/typed entries via Registry.Category and Registry.Table;
wenzelm
parents:
78940
diff
changeset
|
31 |
def table_value(name: String, table: TOML.Table): A |
409442cb7814
support interpreted/typed entries via Registry.Category and Registry.Table;
wenzelm
parents:
78940
diff
changeset
|
32 |
override def default_value: A = table_value("", TOML.Table.empty) |
409442cb7814
support interpreted/typed entries via Registry.Category and Registry.Table;
wenzelm
parents:
78940
diff
changeset
|
33 |
override def value(name: String, t: TOML.T): A = |
409442cb7814
support interpreted/typed entries via Registry.Category and Registry.Table;
wenzelm
parents:
78940
diff
changeset
|
34 |
t match { |
409442cb7814
support interpreted/typed entries via Registry.Category and Registry.Table;
wenzelm
parents:
78940
diff
changeset
|
35 |
case table: TOML.Table => table_value(name, table) |
409442cb7814
support interpreted/typed entries via Registry.Category and Registry.Table;
wenzelm
parents:
78940
diff
changeset
|
36 |
case _ => err("Table expected", Long_Name.qualify(prefix, name)) |
409442cb7814
support interpreted/typed entries via Registry.Category and Registry.Table;
wenzelm
parents:
78940
diff
changeset
|
37 |
} |
409442cb7814
support interpreted/typed entries via Registry.Category and Registry.Table;
wenzelm
parents:
78940
diff
changeset
|
38 |
} |
78945
73162a487f94
build cluster host specifications are based on registry entries (table prefix "host");
wenzelm
parents:
78942
diff
changeset
|
39 |
|
78950 | 40 |
|
41 |
/* build cluster resources */ |
|
42 |
||
78945
73162a487f94
build cluster host specifications are based on registry entries (table prefix "host");
wenzelm
parents:
78942
diff
changeset
|
43 |
object Host extends Table[List[Options.Spec]]("host") { |
73162a487f94
build cluster host specifications are based on registry entries (table prefix "host");
wenzelm
parents:
78942
diff
changeset
|
44 |
def options_spec(a: TOML.Key, b: TOML.T): Option[Options.Spec] = |
78947 | 45 |
TOML.Scalar.unapply(b).map(Options.Spec.eq(a, _)) |
78945
73162a487f94
build cluster host specifications are based on registry entries (table prefix "host");
wenzelm
parents:
78942
diff
changeset
|
46 |
|
73162a487f94
build cluster host specifications are based on registry entries (table prefix "host");
wenzelm
parents:
78942
diff
changeset
|
47 |
override def table_value(a: String, t: TOML.Table): List[Options.Spec] = |
73162a487f94
build cluster host specifications are based on registry entries (table prefix "host");
wenzelm
parents:
78942
diff
changeset
|
48 |
for ((a, b) <- t.any.values; s <- options_spec(a, b)) yield s |
73162a487f94
build cluster host specifications are based on registry entries (table prefix "host");
wenzelm
parents:
78942
diff
changeset
|
49 |
} |
78939 | 50 |
} |
51 |
||
78942
409442cb7814
support interpreted/typed entries via Registry.Category and Registry.Table;
wenzelm
parents:
78940
diff
changeset
|
52 |
class Registry private(val table: TOML.Table) { |
409442cb7814
support interpreted/typed entries via Registry.Category and Registry.Table;
wenzelm
parents:
78940
diff
changeset
|
53 |
override def toString: String = TOML.Format(table) |
409442cb7814
support interpreted/typed entries via Registry.Category and Registry.Table;
wenzelm
parents:
78940
diff
changeset
|
54 |
|
409442cb7814
support interpreted/typed entries via Registry.Category and Registry.Table;
wenzelm
parents:
78940
diff
changeset
|
55 |
def get[A](category: Registry.Category[A], name: String): A = { |
409442cb7814
support interpreted/typed entries via Registry.Category and Registry.Table;
wenzelm
parents:
78940
diff
changeset
|
56 |
table.any.get(category.prefix) match { |
409442cb7814
support interpreted/typed entries via Registry.Category and Registry.Table;
wenzelm
parents:
78940
diff
changeset
|
57 |
case None => category.default_value |
409442cb7814
support interpreted/typed entries via Registry.Category and Registry.Table;
wenzelm
parents:
78940
diff
changeset
|
58 |
case Some(t: TOML.Table) => |
409442cb7814
support interpreted/typed entries via Registry.Category and Registry.Table;
wenzelm
parents:
78940
diff
changeset
|
59 |
t.any.get(name) match { |
409442cb7814
support interpreted/typed entries via Registry.Category and Registry.Table;
wenzelm
parents:
78940
diff
changeset
|
60 |
case None => category.default_value |
409442cb7814
support interpreted/typed entries via Registry.Category and Registry.Table;
wenzelm
parents:
78940
diff
changeset
|
61 |
case Some(u) => category.value(name, u) |
409442cb7814
support interpreted/typed entries via Registry.Category and Registry.Table;
wenzelm
parents:
78940
diff
changeset
|
62 |
} |
409442cb7814
support interpreted/typed entries via Registry.Category and Registry.Table;
wenzelm
parents:
78940
diff
changeset
|
63 |
case Some(_) => Registry.err("Table expected", category.prefix) |
409442cb7814
support interpreted/typed entries via Registry.Category and Registry.Table;
wenzelm
parents:
78940
diff
changeset
|
64 |
} |
409442cb7814
support interpreted/typed entries via Registry.Category and Registry.Table;
wenzelm
parents:
78940
diff
changeset
|
65 |
} |
78940 | 66 |
} |