src/Pure/Thy/export.ML

 (*  Title:      Pure/Thy/export.ML
     Author:     Makarius
 
-Manage theory exports.
+Manage theory exports: compressed blobs.
 *)
 
 signature EXPORT =
 sig
-  val export: theory -> string -> Output.output -> unit
-  val export_uncompressed: theory -> string -> Output.output -> unit
+  val export: theory -> string -> string -> unit
+  val export_raw: theory -> string -> string list -> unit
 end;
 
 structure Export: EXPORT =
 struct
 
-fun gen_export compress thy name output =
+fun gen_export compress thy name body =
   (Output.try_protocol_message o Markup.export)
    {id = Position.get_id (Position.thread_data ()),
     serial = serial (),
     theory_name = Context.theory_long_name thy,
     name = name,
-    compress = compress} [output];
+    compress = compress} body;
 
-val export = gen_export true;
-val export_uncompressed = gen_export false;
+fun export thy name body = gen_export (size body > 60) thy name [body];
+fun export_raw thy name body = gen_export false thy name body;
 
 end;