# HG changeset patch
# User wenzelm
# Date 1237825302 -3600
# Node ID 9bb872667af6994ade070d326d646e83850288f6
# Parent  6de7ef888aa3b7a1a2a820ba639cdb460b5a39e4
suppress status output for traditional tty modes (including Proof General);
keyword report: explicitly issue message on writeln channel as well;

diff -r 6de7ef888aa3 -r 9bb872667af6 src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Mon Mar 23 17:20:31 2009 +0100
+++ b/src/Pure/General/output.ML	Mon Mar 23 17:21:42 2009 +0100
@@ -101,7 +101,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);
+val status_fn = ref (fn _: string => ());
 
 fun writeln s = ! writeln_fn (output s);
 fun priority s = ! priority_fn (output s);
diff -r 6de7ef888aa3 -r 9bb872667af6 src/Pure/Isar/outer_keyword.ML
--- a/src/Pure/Isar/outer_keyword.ML	Mon Mar 23 17:20:31 2009 +0100
+++ b/src/Pure/Isar/outer_keyword.ML	Mon Mar 23 17:21:42 2009 +0100
@@ -150,23 +150,25 @@
   Pretty.mark (Markup.command_decl name (kind_of kind))
     (Pretty.str ("Outer syntax command: " ^ quote name ^ " (" ^ kind_of kind ^ ")"));
 
+fun status_writeln s = (Output.status s; writeln s);
+
 fun report () =
   let val (keywords, commands) = CRITICAL (fn () =>
     (dest_keywords (), sort_wrt #1 (Symtab.dest (get_commands ()))))
   in map report_keyword keywords @ map report_command commands end
-  |> Pretty.chunks |> Pretty.string_of |> Output.status;
+  |> Pretty.chunks |> Pretty.string_of |> status_writeln;
 
 
 (* augment tables *)
 
 fun keyword name =
  (change_lexicons (apfst (Scan.extend_lexicon (Symbol.explode name)));
-  Output.status (Pretty.string_of (report_keyword name)));
+  status_writeln (Pretty.string_of (report_keyword name)));
 
 fun command name kind =
  (change_lexicons (apsnd (Scan.extend_lexicon (Symbol.explode name)));
   change_commands (Symtab.update (name, kind));
-  Output.status (Pretty.string_of (report_command (name, kind))));
+  status_writeln (Pretty.string_of (report_command (name, kind))));
 
 
 (* command categories *)
diff -r 6de7ef888aa3 -r 9bb872667af6 src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Mon Mar 23 17:20:31 2009 +0100
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Mon Mar 23 17:21:42 2009 +0100
@@ -76,7 +76,7 @@
 
 fun setup_messages () =
  (Output.writeln_fn := message "" "" "";
-  Output.status_fn := (fn s => ! Output.priority_fn s);
+  Output.status_fn := (fn _ => ());
   Output.priority_fn := message (special "I") (special "J") "";
   Output.tracing_fn := message (special "I" ^ special "V") (special "J") "";
   Output.debug_fn := message (special "K") (special "L") "+++ ";