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