src/Pure/General/output.ML
changeset 70662 0f9a4e8ee1ab
parent 65301 fca593a62785
child 70907 7e3f25a0cee4
--- 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);