--- a/src/Pure/Thy/export.scala Fri Jan 11 11:05:36 2019 +0100
+++ b/src/Pure/Thy/export.scala Fri Jan 11 11:28:04 2019 +0100
@@ -75,6 +75,15 @@
{
override def toString: String = compound_name(theory_name, name)
+ def uncompressed(cache: XZ.Cache = XZ.cache()): Bytes =
+ {
+ val (compressed, bytes) = body.join
+ if (compressed) bytes.uncompress(cache = cache) else bytes
+ }
+
+ def uncompressed_yxml(cache: XZ.Cache = XZ.cache()): XML.Body =
+ YXML.parse_body(UTF8.decode_permissive(uncompressed(cache = cache)))
+
def write(db: SQL.Database)
{
val (compressed, bytes) = body.join
@@ -88,15 +97,6 @@
stmt.execute()
})
}
-
- def uncompressed(cache: XZ.Cache = XZ.cache()): Bytes =
- {
- val (compressed, bytes) = body.join
- if (compressed) bytes.uncompress(cache = cache) else bytes
- }
-
- def uncompressed_yxml(cache: XZ.Cache = XZ.cache()): XML.Body =
- YXML.parse_body(UTF8.decode_permissive(uncompressed(cache = cache)))
}
def make_regex(pattern: String): Regex =