# HG changeset patch
# User wenzelm
# Date 1216124149 -7200
# Node ID 2c281958e45d8b11fcdbadede2e6f610d78e059e
# Parent  6c347b96d9414ed75307d4291ee220b4d90679d3
added status channel;
writeln_default: suppress empty messages;

diff -r 6c347b96d941 -r 2c281958e45d src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Tue Jul 15 14:15:43 2008 +0200
+++ b/src/Pure/General/output.ML	Tue Jul 15 14:15:49 2008 +0200
@@ -42,8 +42,10 @@
   val error_fn: (output -> unit) ref
   val debug_fn: (output -> unit) ref
   val prompt_fn: (output -> unit) ref
+  val status_fn: (output -> unit) ref
   val error_msg: string -> unit
   val prompt: string -> unit
+  val status: string -> unit
   val debugging: bool ref
   val no_warnings: ('a -> 'b) -> 'a -> 'b
   val debug: (unit -> string) -> unit
@@ -89,7 +91,9 @@
   (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr));
 
 val immediate_output = std_output o output;
-val writeln_default = std_output o suffix "\n";
+
+fun writeln_default "" = ()
+  | writeln_default s = std_output (suffix "\n" s);
 
 
 (* Isabelle output channels *)
@@ -101,6 +105,7 @@
 val error_fn = ref (std_output o suffix "\n" o prefix_lines "*** ");
 val debug_fn = ref (std_output o suffix "\n" o prefix_lines "::: ");
 val prompt_fn = ref std_output;
+val status_fn = ref (fn s => ! writeln_fn s);
 
 fun writeln s = ! writeln_fn (output s);
 fun priority s = ! priority_fn (output s);
@@ -108,6 +113,7 @@
 fun warning s = ! warning_fn (output s);
 fun error_msg s = ! error_fn (output s);
 fun prompt s = ! prompt_fn (output s);
+fun status s = ! status_fn (output s);
 
 val tolerate_legacy_features = ref true;
 fun legacy_feature s =