# 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 "");