1.1 --- a/src/Pure/System/isabelle_process.ML	Fri Sep 17 20:42:26 2010 +0200
     1.2 +++ b/src/Pure/System/isabelle_process.ML	Fri Sep 17 20:56:32 2010 +0200
     1.3 @@ -62,9 +62,10 @@
     1.4  
     1.5  in
     1.6  
     1.7 -fun standard_message out_stream ch body =
     1.8 +fun standard_message out_stream with_serial ch body =
     1.9    message out_stream ch
    1.10 -    ((Markup.serialN, serial_string ()) :: Position.properties_of (Position.thread_data ())) body;
    1.11 +    ((if with_serial then cons (Markup.serialN, serial_string ()) else I)
    1.12 +      (Position.properties_of (Position.thread_data ()))) body;
    1.13  
    1.14  fun init_message out_stream =
    1.15    message out_stream "A" [(Markup.pidN, process_id ())] (Session.welcome ());
    1.16 @@ -102,13 +103,13 @@
    1.17      val _ = Simple_Thread.fork false (auto_flush TextIO.stdOut);
    1.18      val _ = Simple_Thread.fork false (auto_flush TextIO.stdErr);
    1.19    in
    1.20 -    Output.status_fn   := standard_message out_stream "B";
    1.21 -    Output.report_fn   := standard_message out_stream "C";
    1.22 -    Output.writeln_fn  := standard_message out_stream "D";
    1.23 -    Output.tracing_fn  := standard_message out_stream "E";
    1.24 -    Output.warning_fn  := standard_message out_stream "F";
    1.25 -    Output.error_fn    := standard_message out_stream "G";
    1.26 -    Output.debug_fn    := standard_message out_stream "H";
    1.27 +    Output.status_fn   := standard_message out_stream false "B";
    1.28 +    Output.report_fn   := standard_message out_stream false "C";
    1.29 +    Output.writeln_fn  := standard_message out_stream true "D";
    1.30 +    Output.tracing_fn  := standard_message out_stream true "E";
    1.31 +    Output.warning_fn  := standard_message out_stream true "F";
    1.32 +    Output.error_fn    := standard_message out_stream true "G";
    1.33 +    Output.debug_fn    := standard_message out_stream true "H";
    1.34      Output.priority_fn := ! Output.writeln_fn;
    1.35      Output.prompt_fn   := ignore;
    1.36      (in_stream, out_stream)