# HG changeset patch # User wenzelm # Date 1672497733 -3600 # Node ID 2915740fce1f619cebba9e733159a61fb379c91f # Parent 69f6895dd7d45b13cd5f9112938a852d03bc31f6 tunes signature; diff -r 69f6895dd7d4 -r 2915740fce1f src/Pure/Thy/export.scala --- 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) } diff -r 69f6895dd7d4 -r 2915740fce1f src/Pure/Thy/export_theory.scala --- 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() diff -r 69f6895dd7d4 -r 2915740fce1f src/Pure/Tools/build_job.scala --- 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 { diff -r 69f6895dd7d4 -r 2915740fce1f src/Pure/Tools/dump.scala --- 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) diff -r 69f6895dd7d4 -r 2915740fce1f src/Pure/Tools/server_commands.scala --- 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) } })) diff -r 69f6895dd7d4 -r 2915740fce1f src/Tools/jEdit/src/isabelle_export.scala --- 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() }