src/Pure/PIDE/resources.ML

   val provide_parse_files: string -> (theory -> Token.file list * theory) parser
   val loaded_files_current: theory -> bool
   val check_path: Proof.context -> Path.T -> string * Position.T -> Path.T
   val check_file: Proof.context -> Path.T -> string * Position.T -> Path.T
   val check_dir: Proof.context -> Path.T -> string * Position.T -> Path.T
-  val export: {theory_name: string, path: string, compress: bool} -> Output.output list -> unit
+  val export_message: Markup.export_args -> Output.output list -> unit
+  val export: theory -> string -> Output.output -> unit
 end;
 
 structure Resources: RESOURCES =
 struct
 

 end;
 
 
 (* export *)
 
-fun export {theory_name, path, compress} output =
-  let
-    val props =
-      Markup.export
-        {id = Position.get_id (Position.thread_data ()),
-          theory_name = theory_name, path = path, compress = compress};
-  in Output.try_protocol_message props output end;
+val export_message = Output.try_protocol_message o Markup.export;
+
+fun export thy path output =
+  export_message
+   {id = Position.get_id (Position.thread_data ()),
+    theory_name = Context.theory_long_name thy,
+    path = path,
+    compress = true} [output];
 
 end;