tuned signature;

--- a/src/Pure/PIDE/markup.ML	Sat May 05 22:33:35 2018 +0200
+++ b/src/Pure/PIDE/markup.ML	Sun May 06 19:10:21 2018 +0200
@@ -203,7 +203,8 @@
   val command_timing: Properties.entry
   val theory_timing: Properties.entry
   val exportN: string
-  val export: {id: string option, theory_name: string, path: string, compress: bool} -> Properties.T
+  type export_args = {id: string option, theory_name: string, path: string, compress: bool}
+  val export: export_args -> Properties.T
   val loading_theory: string -> Properties.T
   val dest_loading_theory: Properties.T -> string option
   val build_session_finished: Properties.T
@@ -641,7 +642,8 @@
 val theory_timing = (functionN, "theory_timing");
 
 val exportN = "export";
-fun export {id, theory_name, path, compress} =
+type export_args = {id: string option, theory_name: string, path: string, compress: bool}
+fun export ({id, theory_name, path, compress}: export_args) =
   [(functionN, exportN), ("id", the_default "" id),
     ("theory_name", theory_name), ("path", path), ("compress", Value.print_bool compress)];
 

--- a/src/Pure/PIDE/resources.ML	Sat May 05 22:33:35 2018 +0200
+++ b/src/Pure/PIDE/resources.ML	Sun May 06 19:10:21 2018 +0200
@@ -36,7 +36,8 @@
   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 =
@@ -299,12 +300,13 @@
 
 (* 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;