--- 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;