author | wenzelm |
Sun, 12 Nov 2023 20:59:23 +0100 | |
changeset 78962 | 7a58c1199de3 |
parent 78961 | 11045cf2b5c2 |
child 78963 | 30360ee939f4 |
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 |
||
78951 | 13 |
def load(files: Iterable[Path]): Registry = new Registry(TOML.parse_files(files)) |
14 |
||
15 |
def global_files(): List[Path] = |
|
78939 | 16 |
Path.split_permissive_files(Isabelle_System.getenv("ISABELLE_REGISTRY")) |
17 |
||
78951 | 18 |
lazy val global: Registry = load(global_files()) |
78942
409442cb7814
support interpreted/typed entries via Registry.Category and Registry.Table;
wenzelm
parents:
78940
diff
changeset
|
19 |
|
78950 | 20 |
|
21 |
/* interpreted entries */ |
|
22 |
||
78962 | 23 |
trait Category { |
24 |
def prefix: String |
|
78942
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) + ")" |
78961 | 26 |
def qualify(name: String): String = Long_Name.qualify(prefix, name) |
27 |
def try_unqualify(name: String): Option[String] = Long_Name.try_unqualify(prefix, name) |
|
28 |
||
78962 | 29 |
type A |
30 |
def bad_value(name: String): Nothing = error("Bad registry entry " + quote(qualify(name))) |
|
78960 | 31 |
def default_value(name: String): A |
78942
409442cb7814
support interpreted/typed entries via Registry.Category and Registry.Table;
wenzelm
parents:
78940
diff
changeset
|
32 |
def value(name: String, t: TOML.T): A |
409442cb7814
support interpreted/typed entries via Registry.Category and Registry.Table;
wenzelm
parents:
78940
diff
changeset
|
33 |
} |
409442cb7814
support interpreted/typed entries via Registry.Category and Registry.Table;
wenzelm
parents:
78940
diff
changeset
|
34 |
|
78962 | 35 |
trait Table extends Category { |
78942
409442cb7814
support interpreted/typed entries via Registry.Category and Registry.Table;
wenzelm
parents:
78940
diff
changeset
|
36 |
def table_value(name: String, table: TOML.Table): A |
78960 | 37 |
override def default_value(name: String): A = table_value(name, TOML.Table.empty) |
78942
409442cb7814
support interpreted/typed entries via Registry.Category and Registry.Table;
wenzelm
parents:
78940
diff
changeset
|
38 |
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
|
39 |
t match { |
409442cb7814
support interpreted/typed entries via Registry.Category and Registry.Table;
wenzelm
parents:
78940
diff
changeset
|
40 |
case table: TOML.Table => table_value(name, table) |
78960 | 41 |
case _ => bad_value(name) |
78942
409442cb7814
support interpreted/typed entries via Registry.Category and Registry.Table;
wenzelm
parents:
78940
diff
changeset
|
42 |
} |
409442cb7814
support interpreted/typed entries via Registry.Category and Registry.Table;
wenzelm
parents:
78940
diff
changeset
|
43 |
} |
78945
73162a487f94
build cluster host specifications are based on registry entries (table prefix "host");
wenzelm
parents:
78942
diff
changeset
|
44 |
|
78950 | 45 |
|
46 |
/* build cluster resources */ |
|
47 |
||
78962 | 48 |
object Host extends Table { |
49 |
val prefix = "host" |
|
50 |
type A = List[Options.Spec] |
|
51 |
||
78945
73162a487f94
build cluster host specifications are based on registry entries (table prefix "host");
wenzelm
parents:
78942
diff
changeset
|
52 |
def options_spec(a: TOML.Key, b: TOML.T): Option[Options.Spec] = |
78947 | 53 |
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
|
54 |
|
78962 | 55 |
override def table_value(a: String, t: TOML.Table): A = |
78945
73162a487f94
build cluster host specifications are based on registry entries (table prefix "host");
wenzelm
parents:
78942
diff
changeset
|
56 |
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
|
57 |
} |
78939 | 58 |
} |
59 |
||
78942
409442cb7814
support interpreted/typed entries via Registry.Category and Registry.Table;
wenzelm
parents:
78940
diff
changeset
|
60 |
class Registry private(val table: TOML.Table) { |
78959 | 61 |
override def toString: String = |
62 |
(for (a <- table.domain.toList.sorted.iterator) yield { |
|
63 |
val size = |
|
64 |
table.any.get(a) match { |
|
65 |
case Some(t: TOML.Array) => "(" + t.length + ")" |
|
66 |
case Some(t: TOML.Table) => "(" + t.domain.size + ")" |
|
67 |
case _ => "" |
|
68 |
} |
|
69 |
a + size |
|
70 |
}).mkString("Registry(", ", ", ")") |
|
78942
409442cb7814
support interpreted/typed entries via Registry.Category and Registry.Table;
wenzelm
parents:
78940
diff
changeset
|
71 |
|
78962 | 72 |
def get(category: Registry.Category, name: String): category.A = { |
78942
409442cb7814
support interpreted/typed entries via Registry.Category and Registry.Table;
wenzelm
parents:
78940
diff
changeset
|
73 |
table.any.get(category.prefix) match { |
78960 | 74 |
case None => category.default_value(name) |
78942
409442cb7814
support interpreted/typed entries via Registry.Category and Registry.Table;
wenzelm
parents:
78940
diff
changeset
|
75 |
case Some(t: TOML.Table) => |
409442cb7814
support interpreted/typed entries via Registry.Category and Registry.Table;
wenzelm
parents:
78940
diff
changeset
|
76 |
t.any.get(name) match { |
78960 | 77 |
case None => category.default_value(name) |
78942
409442cb7814
support interpreted/typed entries via Registry.Category and Registry.Table;
wenzelm
parents:
78940
diff
changeset
|
78 |
case Some(u) => category.value(name, u) |
409442cb7814
support interpreted/typed entries via Registry.Category and Registry.Table;
wenzelm
parents:
78940
diff
changeset
|
79 |
} |
78960 | 80 |
case Some(_) => category.bad_value(name) |
78942
409442cb7814
support interpreted/typed entries via Registry.Category and Registry.Table;
wenzelm
parents:
78940
diff
changeset
|
81 |
} |
409442cb7814
support interpreted/typed entries via Registry.Category and Registry.Table;
wenzelm
parents:
78940
diff
changeset
|
82 |
} |
78940 | 83 |
} |