# HG changeset patch
# User wenzelm
# Date 1567781308 -7200
# Node ID 0f9a4e8ee1abf74a726aa900a75a7df78be2d6e2
# Parent  9c4809ec28ef7ea290356b1f1e152e070543062c
tuned signature -- prefer bulk messages;

diff -r 9c4809ec28ef -r 0f9a4e8ee1ab src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Fri Sep 06 16:11:19 2019 +0200
+++ b/src/Pure/General/output.ML	Fri Sep 06 16:48:28 2019 +0200
@@ -35,7 +35,7 @@
   val error_message': serial * string -> unit
   val error_message: string -> unit
   val system_message: string -> unit
-  val status: string -> unit
+  val status: string list -> unit
   val report: string list -> unit
   val result: Properties.T -> string list -> unit
   val protocol_message: Properties.T -> string list -> unit
@@ -146,7 +146,7 @@
 fun error_message' (i, s) = ! error_message_fn (i, [output s]);
 fun error_message s = error_message' (serial (), s);
 fun system_message s = ! system_message_fn [output s];
-fun status s = ! status_fn [output s];
+fun status ss = ! status_fn (map output ss);
 fun report ss = ! report_fn (map output ss);
 fun result props ss = ! result_fn props (map output ss);
 fun protocol_message props ss = ! protocol_message_fn props (map output ss);
diff -r 9c4809ec28ef -r 0f9a4e8ee1ab src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Fri Sep 06 16:11:19 2019 +0200
+++ b/src/Pure/PIDE/command.ML	Fri Sep 06 16:48:28 2019 +0200
@@ -233,7 +233,7 @@
   Toplevel.setmp_thread_position tr (fn () => Output.report [Markup.markup_only m]) ();
 
 fun status tr m =
-  Toplevel.setmp_thread_position tr (fn () => Output.status (Markup.markup_only m)) ();
+  Toplevel.setmp_thread_position tr (fn () => Output.status [Markup.markup_only m]) ();
 
 fun command_indent tr st =
   (case try Toplevel.proof_of st of
diff -r 9c4809ec28ef -r 0f9a4e8ee1ab src/Pure/PIDE/document.ML
--- 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 =
diff -r 9c4809ec28ef -r 0f9a4e8ee1ab src/Pure/PIDE/execution.ML
--- a/src/Pure/PIDE/execution.ML	Fri Sep 06 16:11:19 2019 +0200
+++ b/src/Pure/PIDE/execution.ML	Fri Sep 06 16:48:28 2019 +0200
@@ -141,7 +141,7 @@
     val props =
       if ! Multithreading.trace >= 2
       then [(Markup.taskN, Task_Queue.str_of_task task)] else [];
-  in Output.status (implode (map (Markup.markup_only o Markup.properties props) markups)) end;
+  in Output.status (map (Markup.markup_only o Markup.properties props) markups) end;
 
 type params = {name: string, pos: Position.T, pri: int};