# HG changeset patch
# User wenzelm
# Date 1547202484 -3600
# Node ID e1188d9d616b608aa1e201d663de4cae9efd648a
# Parent  a2fbfdc5e62d18bbc0ea25556793faa4d5875592
tuned;

diff -r a2fbfdc5e62d -r e1188d9d616b src/Pure/Thy/export.scala
--- 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 =