--- a/src/Pure/PIDE/markup.ML Sat Jan 12 14:56:57 2013 +0100
+++ b/src/Pure/PIDE/markup.ML Sat Jan 12 15:00:48 2013 +0100
@@ -133,6 +133,8 @@
val invoke_scala: string -> string -> Properties.T
val cancel_scala: string -> Properties.T
val ML_statistics: Properties.entry
+ val loading_theory: string -> Properties.T
+ val dest_loading_theory: Properties.T -> string option
val no_output: Output.output * Output.output
val default_output: T -> Output.output * Output.output
val add_mode: string -> (T -> Output.output * Output.output) -> unit
@@ -408,6 +410,11 @@
val ML_statistics = (functionN, "ML_statistics");
+fun loading_theory name = [("function", "loading_theory"), ("name", name)];
+
+fun dest_loading_theory [("function", "loading_theory"), ("name", name)] = SOME name
+ | dest_loading_theory _ = NONE;
+
(** print mode operations **)