src/Pure/PIDE/isabelle_markup.ML

   val malformedN: string val malformed: Markup.T
   val tokenN: string val token: Properties.T -> Markup.T
   val command_spanN: string val command_span: string -> Markup.T
   val ignored_spanN: string val ignored_span: Markup.T
   val malformed_spanN: string val malformed_span: Markup.T
-  val loaded_theoryN: string val loaded_theory: string -> Markup.T
   val elapsedN: string
   val cpuN: string
   val gcN: string
   val timingN: string val timing: Timing.timing -> Markup.T
   val subgoalsN: string

   val reportN: string val report: Markup.T
   val no_reportN: string val no_report: Markup.T
   val badN: string val bad: Markup.T
   val functionN: string
   val ready: Properties.T
+  val loaded_theory: string -> Properties.T
   val assign_execs: Properties.T
   val removed_versions: Properties.T
   val invoke_scala: string -> string -> Properties.T
   val cancel_scala: string -> Properties.T
 end;

 val (command_spanN, command_span) = markup_string "command_span" Markup.nameN;
 val (ignored_spanN, ignored_span) = markup_elem "ignored_span";
 val (malformed_spanN, malformed_span) = markup_elem "malformed_span";
 
 
-(* theory loader *)
-
-val (loaded_theoryN, loaded_theory) = markup_string "loaded_theory" Markup.nameN;
-
-
 (* timing *)
 
 val timingN = "timing";
 val elapsedN = "elapsed";
 val cpuN = "cpu";

 
 val functionN = "function"
 
 val ready = [(functionN, "ready")];
 
+fun loaded_theory name = [(functionN, "loaded_theory"), (Markup.nameN, name)];
+
 val assign_execs = [(functionN, "assign_execs")];
 val removed_versions = [(functionN, "removed_versions")];
 
 fun invoke_scala name id = [(functionN, "invoke_scala"), (Markup.nameN, name), (idN, id)];
 fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)];