src/Pure/PIDE/markup.ML

   val ML_statistics: Properties.entry
   val task_statistics: Properties.entry
   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
   val build_session_finished: Properties.T
   val print_operationsN: string

 val command_timing = (functionN, "command_timing");
 
 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)];
 
 fun dest_loading_theory [("function", "loading_theory"), ("name", name)] = SOME name
   | dest_loading_theory _ = NONE;