--- a/src/Pure/PIDE/markup.ML Sat May 05 21:44:18 2018 +0200
+++ b/src/Pure/PIDE/markup.ML Sat May 05 22:33:35 2018 +0200
@@ -202,6 +202,8 @@
val task_statistics: Properties.entry
val command_timing: Properties.entry
val theory_timing: Properties.entry
+ val exportN: string
+ val export: {id: string option, theory_name: string, path: string, compress: bool} -> Properties.T
val loading_theory: string -> Properties.T
val dest_loading_theory: Properties.T -> string option
val build_session_finished: Properties.T
@@ -638,6 +640,11 @@
val theory_timing = (functionN, "theory_timing");
+val exportN = "export";
+fun export {id, theory_name, path, compress} =
+ [(functionN, exportN), ("id", the_default "" id),
+ ("theory_name", theory_name), ("path", path), ("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