diff -r b95ff3744815 -r 477ca927676f src/Pure/PIDE/markup.ML
--- 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 **)