src/Pure/Thy/thy_info.ML
changeset 73559 22b5ecb53dd9
parent 73046 32edc2b4e243
child 73687 54fe8cc0e1c6
--- a/src/Pure/Thy/thy_info.ML	Sun Apr 11 21:32:09 2021 +0200
+++ b/src/Pure/Thy/thy_info.ML	Sun Apr 11 22:47:55 2021 +0200
@@ -344,7 +344,7 @@
 
     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 () =>
@@ -360,7 +360,7 @@
 
     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