src/Pure/PIDE/document.ML
changeset 70662 0f9a4e8ee1ab
parent 70610 d14ddb1df52c
child 70663 4a358f8c7cb7
--- a/src/Pure/PIDE/document.ML	Fri Sep 06 16:11:19 2019 +0200
+++ b/src/Pure/PIDE/document.ML	Fri Sep 06 16:48:28 2019 +0200
@@ -193,7 +193,7 @@
 val is_consolidated = Lazy.is_finished o get_consolidated;
 
 fun commit_consolidated node =
-  (Lazy.force (get_consolidated node); Output.status (Markup.markup_only Markup.consolidated));
+  (Lazy.force (get_consolidated node); Output.status [Markup.markup_only Markup.consolidated]);
 
 fun could_consolidate node =
   not (is_consolidated node) andalso is_some (finished_result_theory node);
@@ -428,7 +428,7 @@
           handle Inttab.DUP dup => err_dup "command" dup;
       val _ =
         Position.setmp_thread_data (Position.id_only id)
-          (fn () => Output.status (Markup.markup_only Markup.accepted)) ();
+          (fn () => Output.status [Markup.markup_only Markup.accepted]) ();
     in (versions, blobs, commands', execution) end);
 
 fun the_command (State {commands, ...}) command_id =
@@ -619,7 +619,7 @@
       if null parents_reports then [Theory.get_pure ()] else map #1 parents_reports;
     val _ = Position.reports (map #2 parents_reports);
     val thy = Resources.begin_theory master_dir header parents;
-    val _ = Output.status (Markup.markup_only Markup.initialized);
+    val _ = Output.status [Markup.markup_only Markup.initialized];
   in thy end;
 
 fun check_root_theory node =