--- a/src/Pure/Admin/build_history.scala Sat Nov 11 17:44:03 2023 +0000
+++ b/src/Pure/Admin/build_history.scala Sun Nov 12 22:34:08 2023 +0100
@@ -357,7 +357,7 @@
build_info.finished_sessions.flatMap { session_name =>
val heap = isabelle_output + Path.explode(session_name)
if (heap.is_file) {
- Some("Heap " + session_name + " (" + Value.Long(File.space(heap).bytes) + " bytes)")
+ Some("Heap " + session_name + " (" + Value.Long(File.size(heap)) + " bytes)")
}
else None
}
--- a/src/Pure/General/bytes.scala Sat Nov 11 17:44:03 2023 +0000
+++ b/src/Pure/General/bytes.scala Sun Nov 12 22:34:08 2023 +0100
@@ -73,7 +73,7 @@
def read_url(name: String): Bytes = using(Url(name).openStream)(read_stream(_))
def read_file(path: Path, offset: Long = 0L, limit: Long = Long.MaxValue): Bytes = {
- val length = File.space(path).bytes
+ val length = File.size(path)
val start = offset.max(0L)
val len = (length - start).max(0L).min(limit)
if (len > Int.MaxValue) error("Cannot read large file slice: " + Space.bytes(len).print)
--- a/src/Pure/General/file.scala Sat Nov 11 17:44:03 2023 +0000
+++ b/src/Pure/General/file.scala Sun Nov 12 22:34:08 2023 +0100
@@ -408,8 +408,8 @@
}
- /* space */
+ /* strict file size */
- def space(path: Path): Space =
- Space.bytes(path.check_file.file.length)
+ def size(path: Path): Long = path.check_file.file.length
+ def space(path: Path): Space = Space.bytes(size(path))
}
--- a/src/Pure/General/long_name.scala Sat Nov 11 17:44:03 2023 +0000
+++ b/src/Pure/General/long_name.scala Sun Nov 12 22:34:08 2023 +0100
@@ -27,4 +27,12 @@
def base_name(name: String): String =
if (name == "") ""
else explode(name).last
+
+ def try_unqualify(qual: String, name: String): Option[String] = {
+ val m = qual.length
+ val n = name.length
+ if (0 < m && m < n && name.startsWith(qual) && name(m) == separator_char)
+ Some(name.substring(m + 1))
+ else None
+ }
}
--- a/src/Pure/General/mailman.scala Sat Nov 11 17:44:03 2023 +0000
+++ b/src/Pure/General/mailman.scala Sun Nov 12 22:34:08 2023 +0100
@@ -376,15 +376,14 @@
try {
val length = connection.getContentLengthLong
val timestamp = connection.getLastModified
- val file = path.file
- if (file.isFile && file.length == length && file.lastModified == timestamp) None
+ if (path.is_file && File.size(path) == length && path.file.lastModified == timestamp) None
else {
Isabelle_System.make_directory(path.dir)
progress.echo("Getting " + url)
val bytes =
using(connection.getInputStream)(Bytes.read_stream(_, hint = length.toInt max 1024))
- Bytes.write(file, bytes)
- file.setLastModified(timestamp)
+ Bytes.write(path, bytes)
+ path.file.setLastModified(timestamp)
Some(path)
}
}
--- a/src/Pure/General/path.scala Sat Nov 11 17:44:03 2023 +0000
+++ b/src/Pure/General/path.scala Sun Nov 12 22:34:08 2023 +0100
@@ -327,8 +327,8 @@
def is_file: Boolean = file.isFile
def is_dir: Boolean = file.isDirectory
- def check_file: Path = if (is_file) this else error("No such file: " + this)
- def check_dir: Path = if (is_dir) this else error("No such directory: " + this)
+ def check_file: Path = if (is_file) this else error("No such file: " + this.expand)
+ def check_dir: Path = if (is_dir) this else error("No such directory: " + this.expand)
def java_path: JPath = file.toPath
--- a/src/Pure/ML/ml_heap.scala Sat Nov 11 17:44:03 2023 +0000
+++ b/src/Pure/ML/ml_heap.scala Sun Nov 12 22:34:08 2023 +0100
@@ -21,7 +21,7 @@
if (heap.is_file) {
val l = sha1_prefix.length
val m = l + SHA1.digest_length
- val n = heap.file.length
+ val n = File.size(heap)
val bs = Bytes.read_file(heap, offset = n - m)
if (bs.length == m) {
val s = bs.text
@@ -151,7 +151,7 @@
database match {
case None =>
case Some(db) =>
- val size = File.space(heap).bytes - sha1_prefix.length - SHA1.digest_length
+ val size = File.size(heap) - sha1_prefix.length - SHA1.digest_length
val slices = (size.toDouble / slice.toDouble).ceil.toInt
val step = (size.toDouble / slices.toDouble).ceil.toLong
--- a/src/Pure/PIDE/headless.scala Sat Nov 11 17:44:03 2023 +0000
+++ b/src/Pure/PIDE/headless.scala Sun Nov 12 22:34:08 2023 +0100
@@ -92,7 +92,7 @@
def finished: Load_State = Load_State(Nil, Nil, Space.zero)
def count_file(name: Document.Node.Name): Long =
- if (loaded_theory(name)) 0 else File.space(name.path).bytes
+ if (loaded_theory(name)) 0 else File.size(name.path)
}
private case class Load_State(
--- a/src/Pure/System/registry.scala Sat Nov 11 17:44:03 2023 +0000
+++ b/src/Pure/System/registry.scala Sun Nov 12 22:34:08 2023 +0100
@@ -20,49 +20,88 @@
/* interpreted entries */
- def err(msg: String, name: String): Nothing =
- error(msg + " for registry entry " + quote(name))
+ trait Category {
+ def prefix: String
+ override def toString: String = "Registry.Category(" + quote(prefix) + ")"
+ def qualify(name: String): String = Long_Name.qualify(prefix, name)
+ def try_unqualify(name: String): Option[String] = Long_Name.try_unqualify(prefix, name)
+
+ type Value
+ def bad_value(name: String): Nothing = error("Bad registry entry " + quote(qualify(name)))
+ def default_value(registry: Registry, name: String): Value
+ def value(registry: Registry, t: TOML.T, name: String): Value
- abstract class Category[A](val prefix: String) {
- override def toString: String = "Registry.Category(" + quote(prefix) + ")"
- def default_value: A
- def value(name: String, t: TOML.T): A
+ def get(registry: Registry, name: String): Value = {
+ registry.root.any.get(prefix) match {
+ case None => default_value(registry, name)
+ case Some(t: TOML.Table) =>
+ t.any.get(name) match {
+ case None => default_value(registry, name)
+ case Some(u) => value(registry, u, name)
+ }
+ case Some(_) => bad_value(name)
+ }
+ }
}
- abstract class Table[A](prefix: String) extends Category[A](prefix) {
- def table_value(name: String, table: TOML.Table): A
- override def default_value: A = table_value("", TOML.Table.empty)
- override def value(name: String, t: TOML.T): A =
+ trait Strict extends Category {
+ override def default_value(registry: Registry, name: String): Value = bad_value(name)
+ }
+
+ trait Table extends Category {
+ def table_value(registry: Registry, table: TOML.Table, name: String): Value
+ override def default_value(registry: Registry, name: String): Value =
+ table_value(registry, TOML.Table.empty, name)
+ override def value(registry: Registry, t: TOML.T, name: String): Value =
t match {
- case table: TOML.Table => table_value(name, table)
- case _ => err("Table expected", Long_Name.qualify(prefix, name))
+ case table: TOML.Table => table_value(registry, table, name)
+ case _ => bad_value(name)
}
}
/* build cluster resources */
- object Host extends Table[List[Options.Spec]]("host") {
+ trait Host extends Table {
+ def prefix = "host"
+ type Value = List[Options.Spec]
+
def options_spec(a: TOML.Key, b: TOML.T): Option[Options.Spec] =
TOML.Scalar.unapply(b).map(Options.Spec.eq(a, _))
- override def table_value(a: String, t: TOML.Table): List[Options.Spec] =
+ override def table_value(registry: Registry, t: TOML.Table, a: String): Value =
for ((a, b) <- t.any.values; s <- options_spec(a, b)) yield s
}
+ object Host extends Host
+ object Host_Strict extends Host with Strict
+ object Host_Cluster extends Host with Strict { override def prefix = Cluster.prefix }
+
+ object Cluster extends Table with Strict {
+ def prefix = "cluster"
+ def prefix_hosts = "hosts"
+ type Value = List[(String, List[Options.Spec])]
+
+ override def table_value(registry: Registry, t: TOML.Table, a: String): Value = {
+ val hosts =
+ t.array.get(prefix_hosts) match {
+ case Some(arr) => arr.string.values.map(_.rep)
+ case None => bad_value(Long_Name.qualify(a, prefix_hosts))
+ }
+ val cluster_specs = Host_Cluster.get(registry, a)
+ hosts.map(h => (h, Host_Strict.get(registry, h) ::: cluster_specs))
+ }
+ }
}
-class Registry private(val table: TOML.Table) {
- override def toString: String = TOML.Format(table)
-
- def get[A](category: Registry.Category[A], name: String): A = {
- table.any.get(category.prefix) match {
- case None => category.default_value
- case Some(t: TOML.Table) =>
- t.any.get(name) match {
- case None => category.default_value
- case Some(u) => category.value(name, u)
+class Registry private(val root: TOML.Table) {
+ override def toString: String =
+ (for (a <- root.domain.toList.sorted.iterator) yield {
+ val size =
+ root.any.get(a) match {
+ case Some(t: TOML.Array) => "(" + t.length + ")"
+ case Some(t: TOML.Table) => "(" + t.domain.size + ")"
+ case _ => ""
}
- case Some(_) => Registry.err("Table expected", category.prefix)
- }
- }
+ a + size
+ }).mkString("Registry(", ", ", ")")
}
--- a/src/Pure/Tools/build_cluster.scala Sat Nov 11 17:44:03 2023 +0000
+++ b/src/Pure/Tools/build_cluster.scala Sun Nov 12 22:34:08 2023 +0100
@@ -73,16 +73,22 @@
}
catch { case ERROR(msg) => err(msg) }
- for (name <- space_explode(',', names)) yield {
- val base_specs = registry.get(Registry.Host, name)
+ def get_registry(a: String): Registry.Cluster.Value =
+ Registry.Cluster.try_unqualify(a) match {
+ case Some(b) => Registry.Cluster.get(registry, b)
+ case None => List(a -> Registry.Host.get(registry, a))
+ }
+
+ for (name <- space_explode(',', names); (host, host_specs) <- get_registry(name))
+ yield {
val (params, options) =
try {
- val (specs1, specs2) = (base_specs ::: more_specs).partition(is_parameter)
+ val (specs1, specs2) = (host_specs ::: more_specs).partition(is_parameter)
(parameters ++ specs1, { test_options ++ specs2; specs2 })
}
catch { case ERROR(msg) => err(msg) }
- apply(name = name,
+ apply(name = host,
hostname = params.string(HOSTNAME),
user = params.string(USER),
port = params.int(PORT),
--- a/src/Pure/Tools/profiling.scala Sat Nov 11 17:44:03 2023 +0000
+++ b/src/Pure/Tools/profiling.scala Sun Nov 12 22:34:08 2023 +0100
@@ -97,7 +97,7 @@
locales = session.locales,
locale_thms = session.locale_thms,
global_thms = session.global_thms,
- heap_size = Space.bytes(store.the_heap(session_name).file.length),
+ heap_size = File.space(store.the_heap(session_name)),
thys_id_size = session.sizeof_thys_id,
thms_id_size = session.sizeof_thms_id,
terms_size = session.sizeof_terms,