report keywords as singleton messages, control message kind via print mode;
authorwenzelm
Mon Jan 04 19:43:59 2010 +0100 (2010-01-04 ago)
changeset 342438821e3293702
parent 34242 5ccdc8bf3849
child 34252 b589bbbdb1b6
report keywords as singleton messages, control message kind via print mode;
src/Pure/Isar/outer_keyword.ML
src/Pure/System/isabelle_process.ML
     1.1 --- a/src/Pure/Isar/outer_keyword.ML	Mon Jan 04 18:56:36 2010 +0100
     1.2 +++ b/src/Pure/Isar/outer_keyword.ML	Mon Jan 04 19:43:59 2010 +0100
     1.3 @@ -43,6 +43,7 @@
     1.4    val dest_commands: unit -> string list
     1.5    val command_keyword: string -> T option
     1.6    val command_tags: string -> string list
     1.7 +  val keyword_status_reportN: string
     1.8    val report: unit -> unit
     1.9    val keyword: string -> unit
    1.10    val command: string -> T -> unit
    1.11 @@ -142,33 +143,38 @@
    1.12  
    1.13  (* report *)
    1.14  
    1.15 +val keyword_status_reportN = "keyword_status_report";
    1.16 +
    1.17 +fun report_message s =
    1.18 +  (if print_mode_active keyword_status_reportN then Output.status else writeln) s;
    1.19 +
    1.20  fun report_keyword name =
    1.21 -  Pretty.mark (Markup.keyword_decl name)
    1.22 -    (Pretty.str ("Outer syntax keyword: " ^ quote name));
    1.23 +  report_message (Markup.markup (Markup.keyword_decl name)
    1.24 +    ("Outer syntax keyword: " ^ quote name));
    1.25  
    1.26  fun report_command (name, kind) =
    1.27 -  Pretty.mark (Markup.command_decl name (kind_of kind))
    1.28 -    (Pretty.str ("Outer syntax command: " ^ quote name ^ " (" ^ kind_of kind ^ ")"));
    1.29 -
    1.30 -fun status_writeln s = (Output.status s; writeln s);
    1.31 +  report_message (Markup.markup (Markup.command_decl name (kind_of kind))
    1.32 +    ("Outer syntax command: " ^ quote name ^ " (" ^ kind_of kind ^ ")"));
    1.33  
    1.34  fun report () =
    1.35    let val (keywords, commands) = CRITICAL (fn () =>
    1.36      (dest_keywords (), sort_wrt #1 (Symtab.dest (get_commands ()))))
    1.37 -  in map report_keyword keywords @ map report_command commands end
    1.38 -  |> Pretty.chunks |> Pretty.string_of |> status_writeln;
    1.39 +  in
    1.40 +    List.app report_keyword keywords;
    1.41 +    List.app report_command commands
    1.42 +  end;
    1.43  
    1.44  
    1.45  (* augment tables *)
    1.46  
    1.47  fun keyword name =
    1.48   (change_lexicons (apfst (Scan.extend_lexicon (Symbol.explode name)));
    1.49 -  status_writeln (Pretty.string_of (report_keyword name)));
    1.50 +  report_keyword name);
    1.51  
    1.52  fun command name kind =
    1.53   (change_lexicons (apsnd (Scan.extend_lexicon (Symbol.explode name)));
    1.54    change_commands (Symtab.update (name, kind));
    1.55 -  status_writeln (Pretty.string_of (report_command (name, kind))));
    1.56 +  report_command (name, kind));
    1.57  
    1.58  
    1.59  (* command categories *)
     2.1 --- a/src/Pure/System/isabelle_process.ML	Mon Jan 04 18:56:36 2010 +0100
     2.2 +++ b/src/Pure/System/isabelle_process.ML	Mon Jan 04 19:43:59 2010 +0100
     2.3 @@ -88,7 +88,8 @@
     2.4  (* init *)
     2.5  
     2.6  fun init out =
     2.7 - (Unsynchronized.change print_mode (update (op =) isabelle_processN);
     2.8 + (Unsynchronized.change print_mode
     2.9 +    (fold (update (op =)) [isabelle_processN, OuterKeyword.keyword_status_reportN]);
    2.10    setup_channels out |> init_message;
    2.11    OuterKeyword.report ();
    2.12    Output.status (Markup.markup Markup.ready "");