--- a/src/Pure/Thy/export.ML Thu Apr 04 14:29:49 2019 +0200
+++ b/src/Pure/Thy/export.ML Thu Apr 04 14:30:58 2019 +0200
@@ -6,6 +6,7 @@
signature EXPORT =
sig
+ val report_export: theory -> Path.binding -> unit
type params = {theory: theory, binding: Path.binding, executable: bool, compress: bool}
val export_params: params -> string list -> unit
val export: theory -> Path.binding -> string list -> unit
@@ -21,25 +22,24 @@
(* export *)
+fun report_export thy binding =
+ let
+ val theory_name = Context.theory_long_name thy;
+ val (path, pos) = Path.dest_binding binding;
+ val markup = Markup.export_path (Path.implode (Path.append (Path.basic theory_name) path));
+ in Context_Position.report_generic (Context.Theory thy) pos markup end;
+
type params = {theory: theory, binding: Path.binding, executable: bool, compress: bool};
fun export_params ({theory = thy, binding, executable, compress}: params) blob =
- let
- val theory_name = Context.theory_long_name thy;
- val name = Path.implode_binding binding;
- val (path, pos) = Path.dest_binding binding;
- val _ =
- Context_Position.report_generic (Context.Theory thy) pos
- (Markup.export_path (Path.implode (Path.append (Path.basic theory_name) path)));
- in
- (Output.try_protocol_message o Markup.export)
- {id = Position.get_id (Position.thread_data ()),
- serial = serial (),
- theory_name = theory_name,
- name = name,
- executable = executable,
- compress = compress} blob
- end;
+ (report_export thy binding;
+ (Output.try_protocol_message o Markup.export)
+ {id = Position.get_id (Position.thread_data ()),
+ serial = serial (),
+ theory_name = Context.theory_long_name thy,
+ name = Path.implode_binding binding,
+ executable = executable,
+ compress = compress} blob);
fun export thy binding blob =
export_params {theory = thy, binding = binding, executable = false, compress = true} blob;