src/Pure/Thy/thy_info.ML

     val text_pos = put_id (Path.position thy_path);
     val text_props = Position.properties_of text_pos;
 
     val _ = remove_thy name;
     val _ = writeln ("Loading theory " ^ quote name ^ required_by " " initiators);
-    val _ = Output.try_protocol_message (Markup.loading_theory name @ text_props) (XML.blob [text]);
+    val _ = Output.try_protocol_message (Markup.loading_theory name @ text_props) [XML.blob [text]];
 
     val _ =
       Position.setmp_thread_data (Position.id_only id) (fn () =>
         (parents, map #2 imports) |> ListPair.app (fn (thy, pos) =>
           Context_Position.reports_global thy [(put_id pos, Theory.get_markup thy)])) ();

       eval_thy options dir header text_pos text
         (if name = Context.PureN then [Context.the_global_context ()] else parents);
 
     val timing_result = Timing.result timing_start;
     val timing_props = [Markup.theory_timing, (Markup.nameN, name)];
-    val _  = Output.try_protocol_message (timing_props @ Markup.timing_properties timing_result) []
+    val _ = Output.try_protocol_message (timing_props @ Markup.timing_properties timing_result) []
 
     fun commit () = update_thy deps theory;
   in
     Result {theory = theory, exec_id = exec_id, present = present, commit = commit, weight = weight}
   end;