--- a/src/Pure/PIDE/resources.ML Sat May 05 21:44:18 2018 +0200
+++ b/src/Pure/PIDE/resources.ML Sat May 05 22:33:35 2018 +0200
@@ -36,6 +36,7 @@
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
end;
structure Resources: RESOURCES =
@@ -295,4 +296,15 @@
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;
+
end;