src/Pure/System/isabelle_process.ML
changeset 38236 d8c7be27e01d
parent 38228 ada3ab6b9085
child 38253 3d4e521014f7
--- a/src/Pure/System/isabelle_process.ML	Sun Aug 08 14:22:54 2010 +0200
+++ b/src/Pure/System/isabelle_process.ML	Sun Aug 08 19:36:31 2010 +0200
@@ -72,11 +72,12 @@
     val _ = Simple_Thread.fork false (auto_flush TextIO.stdErr);
   in
     Output.status_fn   := standard_message out_stream "B";
-    Output.writeln_fn  := standard_message out_stream "C";
-    Output.tracing_fn  := standard_message out_stream "D";
-    Output.warning_fn  := standard_message out_stream "E";
-    Output.error_fn    := standard_message out_stream "F";
-    Output.debug_fn    := standard_message out_stream "G";
+    Output.report_fn   := standard_message out_stream "C";
+    Output.writeln_fn  := standard_message out_stream "D";
+    Output.tracing_fn  := standard_message out_stream "E";
+    Output.warning_fn  := standard_message out_stream "F";
+    Output.error_fn    := standard_message out_stream "G";
+    Output.debug_fn    := standard_message out_stream "H";
     Output.priority_fn := ! Output.writeln_fn;
     Output.prompt_fn   := ignore;
     out_stream
@@ -89,10 +90,10 @@
 
 fun init out =
  (Unsynchronized.change print_mode
-    (fold (update op =) [isabelle_processN, Keyword.keyword_status_reportN, Pretty.symbolicN]);
+    (fold (update op =) [isabelle_processN, Keyword.keyword_statusN, Pretty.symbolicN]);
   setup_channels out |> init_message;
   quick_and_dirty := true;  (* FIXME !? *)
-  Keyword.report ();
+  Keyword.status ();
   Output.status (Markup.markup Markup.ready "");
   Isar.toplevel_loop {init = true, welcome = false, sync = true, secure = true});