# HG changeset patch
# User wenzelm
# Date 1262630639 -3600
# Node ID 8821e329370270984b6db5e2b74f3351c8e9bd69
# Parent  5ccdc8bf3849a1e53e862055641ea86cc2522ece
report keywords as singleton messages, control message kind via print mode;

diff -r 5ccdc8bf3849 -r 8821e3293702 src/Pure/Isar/outer_keyword.ML
--- a/src/Pure/Isar/outer_keyword.ML	Mon Jan 04 18:56:36 2010 +0100
+++ b/src/Pure/Isar/outer_keyword.ML	Mon Jan 04 19:43:59 2010 +0100
@@ -43,6 +43,7 @@
   val dest_commands: unit -> string list
   val command_keyword: string -> T option
   val command_tags: string -> string list
+  val keyword_status_reportN: string
   val report: unit -> unit
   val keyword: string -> unit
   val command: string -> T -> unit
@@ -142,33 +143,38 @@
 
 (* report *)
 
+val keyword_status_reportN = "keyword_status_report";
+
+fun report_message s =
+  (if print_mode_active keyword_status_reportN then Output.status else writeln) s;
+
 fun report_keyword name =
-  Pretty.mark (Markup.keyword_decl name)
-    (Pretty.str ("Outer syntax keyword: " ^ quote name));
+  report_message (Markup.markup (Markup.keyword_decl name)
+    ("Outer syntax keyword: " ^ quote name));
 
 fun report_command (name, kind) =
-  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);
+  report_message (Markup.markup (Markup.command_decl name (kind_of kind))
+    ("Outer syntax command: " ^ quote name ^ " (" ^ kind_of kind ^ ")"));
 
 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 |> status_writeln;
+  in
+    List.app report_keyword keywords;
+    List.app report_command commands
+  end;
 
 
 (* augment tables *)
 
 fun keyword name =
  (change_lexicons (apfst (Scan.extend_lexicon (Symbol.explode name)));
-  status_writeln (Pretty.string_of (report_keyword name)));
+  report_keyword name);
 
 fun command name kind =
  (change_lexicons (apsnd (Scan.extend_lexicon (Symbol.explode name)));
   change_commands (Symtab.update (name, kind));
-  status_writeln (Pretty.string_of (report_command (name, kind))));
+  report_command (name, kind));
 
 
 (* command categories *)
diff -r 5ccdc8bf3849 -r 8821e3293702 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Mon Jan 04 18:56:36 2010 +0100
+++ b/src/Pure/System/isabelle_process.ML	Mon Jan 04 19:43:59 2010 +0100
@@ -88,7 +88,8 @@
 (* init *)
 
 fun init out =
- (Unsynchronized.change print_mode (update (op =) isabelle_processN);
+ (Unsynchronized.change print_mode
+    (fold (update (op =)) [isabelle_processN, OuterKeyword.keyword_status_reportN]);
   setup_channels out |> init_message;
   OuterKeyword.report ();
   Output.status (Markup.markup Markup.ready "");