src/Pure/Thy/export.scala

 
   sealed case class Entry(
     session_name: String,
     theory_name: String,
     name: String,
-    compressed: Boolean,
-    body: Future[Bytes])
+    body: Future[(Boolean, Bytes)])
   {
     override def toString: String = compound_name(theory_name, name)
 
     def write(db: SQL.Database)
     {
-      val bytes = body.join
+      val (compressed, bytes) = body.join
       db.using_statement(Data.table.insert())(stmt =>
       {
         stmt.string(1) = session_name
         stmt.string(2) = theory_name
         stmt.string(3) = name

         stmt.bytes(5) = bytes
         stmt.execute()
       })
     }
 
-    def body_uncompressed(cache: XZ.Cache = XZ.cache()): Bytes =
-      if (compressed) body.join.uncompress(cache = cache) else body.join
+    def uncompressed(cache: XZ.Cache = XZ.cache()): Bytes =
+    {
+      val (compressed, bytes) = body.join
+      if (compressed) bytes.uncompress(cache = cache) else bytes
+    }
   }
 
   def make_regex(pattern: String): Regex =
   {
     @tailrec def make(result: List[String], depth: Int, chs: List[Char]): Regex =

   }
 
   def make_entry(session_name: String, args: Markup.Export.Args, body: Bytes,
     cache: XZ.Cache = XZ.cache()): Entry =
   {
-    Entry(session_name, args.theory_name, args.name, args.compress,
-      if (args.compress) Future.fork(body.compress(cache = cache)) else Future.value(body))
+    Entry(session_name, args.theory_name, args.name,
+      if (args.compress) Future.fork(body.maybe_compress(cache = cache))
+      else Future.value((false, body)))
   }
 
   def read_entry(db: SQL.Database, session_name: String, theory_name: String, name: String): Entry =
   {
     val select =

     {
       val res = stmt.execute_query()
       if (res.next()) {
         val compressed = res.bool(Data.compressed)
         val body = res.bytes(Data.body)
-        Entry(session_name, theory_name, name, compressed, Future.value(body))
+        Entry(session_name, theory_name, name, Future.value(compressed, body))
       }
       else error(message("Bad export", theory_name, name))
     })
   }
 

             val entry = read_entry(db, session_name, theory_name, name)
             val path = export_dir + Path.basic(theory_name) + Path.explode(name)
 
             progress.echo("exporting " + path)
             Isabelle_System.mkdirs(path.dir)
-            Bytes.write(path, entry.body_uncompressed(cache = xz_cache))
+            Bytes.write(path, entry.uncompressed(cache = xz_cache))
           }
         }
       }
     })
   })