tuned signature;
clarified modules;

--- a/src/Pure/PIDE/markup.ML	Sun May 06 19:10:21 2018 +0200
+++ b/src/Pure/PIDE/markup.ML	Sun May 06 22:15:52 2018 +0200
@@ -203,7 +203,7 @@
   val command_timing: Properties.entry
   val theory_timing: Properties.entry
   val exportN: string
-  type export_args = {id: string option, theory_name: string, path: string, compress: bool}
+  type export_args = {id: string option, theory_name: string, name: string, compress: bool}
   val export: export_args -> Properties.T
   val loading_theory: string -> Properties.T
   val dest_loading_theory: Properties.T -> string option
@@ -642,10 +642,10 @@
 val theory_timing = (functionN, "theory_timing");
 
 val exportN = "export";
-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)];
+type export_args = {id: string option, theory_name: string, name: string, compress: bool}
+fun export ({id, theory_name, name, compress}: export_args) =
+  [(functionN, exportN), (idN, the_default "" id),
+    ("theory_name", theory_name), (nameN, name), ("compress", Value.print_bool compress)];
 
 fun loading_theory name = [("function", "loading_theory"), ("name", name)];
 

--- a/src/Pure/PIDE/markup.scala	Sun May 06 19:10:21 2018 +0200
+++ b/src/Pure/PIDE/markup.scala	Sun May 06 22:15:52 2018 +0200
@@ -571,25 +571,24 @@
   val EXPORT = "export"
   object Export
   {
-    sealed case class Args(id: Option[String], theory_name: String, path: String, compress: Boolean)
+    sealed case class Args(id: Option[String], theory_name: String, name: String, compress: Boolean)
 
     val THEORY_NAME = "theory_name"
-    val PATH = "path"
     val COMPRESS = "compress"
 
     def dest_inline(props: Properties.T): Option[(Args, Bytes)] =
       props match {
         case
-          List((THEORY_NAME, theory_name), (PATH, path), (COMPRESS, Value.Boolean(compress)),
-            (EXPORT, hex)) => Some((Args(None, theory_name, path, compress), Bytes.hex(hex)))
+          List((THEORY_NAME, theory_name), (NAME, name), (COMPRESS, Value.Boolean(compress)),
+            (EXPORT, hex)) => Some((Args(None, theory_name, name, compress), Bytes.hex(hex)))
         case _ => None
       }
 
     def unapply(props: Properties.T): Option[Args] =
       props match {
         case List((FUNCTION, EXPORT), (ID, id),
-          (THEORY_NAME, theory_name), (PATH, path), (COMPRESS, Value.Boolean(compress))) =>
-            Some(Args(proper_string(id), theory_name, path, compress))
+          (THEORY_NAME, theory_name), (PATH, name), (COMPRESS, Value.Boolean(compress))) =>
+            Some(Args(proper_string(id), theory_name, name, compress))
         case _ => None
       }
   }

--- a/src/Pure/PIDE/resources.ML	Sun May 06 19:10:21 2018 +0200
+++ b/src/Pure/PIDE/resources.ML	Sun May 06 22:15:52 2018 +0200
@@ -36,8 +36,6 @@
   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_message: Markup.export_args -> Output.output list -> unit
-  val export: theory -> string -> Output.output -> unit
 end;
 
 structure Resources: RESOURCES =
@@ -297,16 +295,4 @@
 
 end;
 
-
-(* export *)
-
-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;

--- a/src/Pure/ROOT.ML	Sun May 06 19:10:21 2018 +0200
+++ b/src/Pure/ROOT.ML	Sun May 06 22:15:52 2018 +0200
@@ -300,6 +300,7 @@
 ML_file "PIDE/command.ML";
 ML_file "PIDE/query_operation.ML";
 ML_file "PIDE/resources.ML";
+ML_file "Thy/export.ML";
 ML_file "Thy/present.ML";
 ML_file "Thy/thy_info.ML";
 ML_file "Thy/sessions.ML";

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/export.ML	Sun May 06 22:15:52 2018 +0200
@@ -0,0 +1,26 @@
+(*  Title:      Pure/Thy/export.ML
+    Author:     Makarius
+
+Manage theory exports.
+*)
+
+signature EXPORT =
+sig
+  val export: theory -> string -> Output.output -> unit
+  val export_uncompressed: theory -> string -> Output.output -> unit
+end;
+
+structure Export: EXPORT =
+struct
+
+fun gen_export compress thy name output =
+  (Output.try_protocol_message o Markup.export)
+   {id = Position.get_id (Position.thread_data ()),
+    theory_name = Context.theory_long_name thy,
+    name = name,
+    compress = compress} [output];
+
+val export = gen_export true;
+val export_uncompressed = gen_export false;
+
+end;