src/Pure/System/isabelle_process.ML
changeset 38236 d8c7be27e01d
parent 38228 ada3ab6b9085
child 38253 3d4e521014f7
     1.1 --- a/src/Pure/System/isabelle_process.ML	Sun Aug 08 14:22:54 2010 +0200
     1.2 +++ b/src/Pure/System/isabelle_process.ML	Sun Aug 08 19:36:31 2010 +0200
     1.3 @@ -72,11 +72,12 @@
     1.4      val _ = Simple_Thread.fork false (auto_flush TextIO.stdErr);
     1.5    in
     1.6      Output.status_fn   := standard_message out_stream "B";
     1.7 -    Output.writeln_fn  := standard_message out_stream "C";
     1.8 -    Output.tracing_fn  := standard_message out_stream "D";
     1.9 -    Output.warning_fn  := standard_message out_stream "E";
    1.10 -    Output.error_fn    := standard_message out_stream "F";
    1.11 -    Output.debug_fn    := standard_message out_stream "G";
    1.12 +    Output.report_fn   := standard_message out_stream "C";
    1.13 +    Output.writeln_fn  := standard_message out_stream "D";
    1.14 +    Output.tracing_fn  := standard_message out_stream "E";
    1.15 +    Output.warning_fn  := standard_message out_stream "F";
    1.16 +    Output.error_fn    := standard_message out_stream "G";
    1.17 +    Output.debug_fn    := standard_message out_stream "H";
    1.18      Output.priority_fn := ! Output.writeln_fn;
    1.19      Output.prompt_fn   := ignore;
    1.20      out_stream
    1.21 @@ -89,10 +90,10 @@
    1.22  
    1.23  fun init out =
    1.24   (Unsynchronized.change print_mode
    1.25 -    (fold (update op =) [isabelle_processN, Keyword.keyword_status_reportN, Pretty.symbolicN]);
    1.26 +    (fold (update op =) [isabelle_processN, Keyword.keyword_statusN, Pretty.symbolicN]);
    1.27    setup_channels out |> init_message;
    1.28    quick_and_dirty := true;  (* FIXME !? *)
    1.29 -  Keyword.report ();
    1.30 +  Keyword.status ();
    1.31    Output.status (Markup.markup Markup.ready "");
    1.32    Isar.toplevel_loop {init = true, welcome = false, sync = true, secure = true});
    1.33