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