--- a/src/Pure/Thy/export.scala Sat Dec 31 15:32:12 2022 +0100
+++ b/src/Pure/Thy/export.scala Sat Dec 31 15:42:13 2022 +0100
@@ -156,25 +156,24 @@
def name_extends(elems: List[String]): Boolean =
name_elems.startsWith(elems) && name_elems != elems
- def text: String = uncompressed.text
-
- def uncompressed: Bytes = {
- val (compressed, bytes) = body.join
- if (compressed) bytes.uncompress(cache = cache.compress) else bytes
+ def bytes: Bytes = {
+ val (compressed, bs) = body.join
+ if (compressed) bs.uncompress(cache = cache.compress) else bs
}
- def uncompressed_yxml: XML.Body =
- YXML.parse_body(UTF8.decode_permissive(uncompressed), cache = cache)
+ def text: String = bytes.text
+
+ def yxml: XML.Body = YXML.parse_body(UTF8.decode_permissive(bytes), cache = cache)
def write(db: SQL.Database): Unit = {
- val (compressed, bytes) = body.join
+ val (compressed, bs) = body.join
db.using_statement(Data.table.insert()) { stmt =>
stmt.string(1) = session_name
stmt.string(2) = theory_name
stmt.string(3) = name
stmt.bool(4) = executable
stmt.bool(5) = compressed
- stmt.bytes(6) = bytes
+ stmt.bytes(6) = bs
stmt.execute()
}
}
@@ -433,7 +432,7 @@
entry_name <- entry_names(session = session).iterator
if matcher(entry_name)
entry <- get(entry_name.theory, entry_name.name).iterator
- } yield File.content(entry.entry_name.make_path(), entry.uncompressed)).toList
+ } yield File.content(entry.entry_name.make_path(), entry.bytes)).toList
}
override def toString: String =
@@ -453,7 +452,7 @@
def uncompressed_yxml(name: String): XML.Body =
get(name) match {
- case Some(entry) => entry.uncompressed_yxml
+ case Some(entry) => entry.yxml
case None => Nil
}
@@ -505,7 +504,7 @@
val path = export_dir + entry_name.make_path(prune = export_prune)
progress.echo("export " + path + (if (entry.executable) " (executable)" else ""))
Isabelle_System.make_directory(path.dir)
- val bytes = entry.uncompressed
+ val bytes = entry.bytes
if (!path.is_file || Bytes.read(path) != bytes) Bytes.write(path, bytes)
File.set_executable(path, entry.executable)
}
--- a/src/Pure/Thy/export_theory.scala Sat Dec 31 15:32:12 2022 +0100
+++ b/src/Pure/Thy/export_theory.scala Sat Dec 31 15:42:13 2022 +0100
@@ -103,7 +103,7 @@
def read_theory_parents(theory_context: Export.Theory_Context): Option[List[String]] =
theory_context.get(Export.THEORY_PREFIX + "parents")
- .map(entry => Library.trim_split_lines(entry.uncompressed.text))
+ .map(entry => Library.trim_split_lines(entry.bytes.text))
def theory_names(
session_context: Export.Session_Context,
@@ -393,7 +393,7 @@
for { entry <- theory_context.get(Export.PROOFS_PREFIX + id.serial) }
yield {
- val body = entry.uncompressed_yxml
+ val body = entry.yxml
val (typargs, (args, (prop_body, proof_body))) = {
import XML.Decode._
import Term_XML.Decode._
@@ -753,7 +753,7 @@
def read_others(theory_context: Export.Theory_Context): Map[String, List[Entity[Other]]] = {
val kinds =
theory_context.get(Export.THEORY_PREFIX + "other_kinds") match {
- case Some(entry) => split_lines(entry.uncompressed.text)
+ case Some(entry) => split_lines(entry.bytes.text)
case None => Nil
}
val other = Other()
--- a/src/Pure/Tools/build_job.scala Sat Dec 31 15:32:12 2022 +0100
+++ b/src/Pure/Tools/build_job.scala Sat Dec 31 15:42:13 2022 +0100
@@ -22,7 +22,7 @@
def read_xml(name: String): XML.Body =
YXML.parse_body(
- Symbol.output(unicode_symbols, UTF8.decode_permissive(read(name).uncompressed)),
+ Symbol.output(unicode_symbols, UTF8.decode_permissive(read(name).bytes)),
cache = theory_context.cache)
for {
--- a/src/Pure/Tools/dump.scala Sat Dec 31 15:32:12 2022 +0100
+++ b/src/Pure/Tools/dump.scala Sat Dec 31 15:42:13 2022 +0100
@@ -57,13 +57,13 @@
for {
entry <- args.snapshot.exports
if entry.name_has_prefix(Export.DOCUMENT_PREFIX)
- } args.write(Path.explode(entry.name), entry.uncompressed)),
+ } args.write(Path.explode(entry.name), entry.bytes)),
Aspect("theory", "foundational theory content",
args =>
for {
entry <- args.snapshot.exports
if entry.name_has_prefix(Export.THEORY_PREFIX)
- } args.write(Path.explode(entry.name), entry.uncompressed),
+ } args.write(Path.explode(entry.name), entry.bytes),
options = List("export_theory"))
).sortBy(_.name)
--- a/src/Pure/Tools/server_commands.scala Sat Dec 31 15:32:12 2022 +0100
+++ b/src/Pure/Tools/server_commands.scala Sat Dec 31 15:42:13 2022 +0100
@@ -266,7 +266,7 @@
val matcher = Export.make_matcher(List(args.export_pattern))
for { entry <- snapshot.exports if matcher(entry.entry_name) }
yield {
- val (base64, body) = entry.uncompressed.maybe_encode_base64
+ val (base64, body) = entry.bytes.maybe_encode_base64
JSON.Object("name" -> entry.name, "base64" -> base64, "body" -> body)
}
}))
--- a/src/Tools/jEdit/src/isabelle_export.scala Sat Dec 31 15:32:12 2022 +0100
+++ b/src/Tools/jEdit/src/isabelle_export.scala Sat Dec 31 15:42:13 2022 +0100
@@ -56,7 +56,7 @@
} yield {
val is_dir = entry.name_elems.length > depth
val path = Export.implode_name(theory :: entry.name_elems.take(depth))
- val file_size = if (is_dir) None else Some(entry.uncompressed.length.toLong)
+ val file_size = if (is_dir) None else Some(entry.bytes.length.toLong)
(path, file_size)
}).toSet.toList
(for ((path, file_size) <- entries.iterator) yield {
@@ -86,7 +86,7 @@
if node_name.theory == theory
(_, entry) <- snapshot.state.node_exports(version, node_name).iterator
if entry.name_elems == name_elems
- } yield entry.uncompressed).find(_ => true).getOrElse(Bytes.empty)
+ } yield entry.bytes).find(_ => true).getOrElse(Bytes.empty)
bytes.stream()
}