src/Pure/System/isabelle_process.ML
changeset 39509 cab2719398a7
parent 39234 d76a2fd129b5
child 39513 fce2202892c4
--- a/src/Pure/System/isabelle_process.ML	Fri Sep 17 20:42:26 2010 +0200
+++ b/src/Pure/System/isabelle_process.ML	Fri Sep 17 20:56:32 2010 +0200
@@ -62,9 +62,10 @@
 
 in
 
-fun standard_message out_stream ch body =
+fun standard_message out_stream with_serial ch body =
   message out_stream ch
-    ((Markup.serialN, serial_string ()) :: Position.properties_of (Position.thread_data ())) body;
+    ((if with_serial then cons (Markup.serialN, serial_string ()) else I)
+      (Position.properties_of (Position.thread_data ()))) body;
 
 fun init_message out_stream =
   message out_stream "A" [(Markup.pidN, process_id ())] (Session.welcome ());
@@ -102,13 +103,13 @@
     val _ = Simple_Thread.fork false (auto_flush TextIO.stdOut);
     val _ = Simple_Thread.fork false (auto_flush TextIO.stdErr);
   in
-    Output.status_fn   := standard_message out_stream "B";
-    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.status_fn   := standard_message out_stream false "B";
+    Output.report_fn   := standard_message out_stream false "C";
+    Output.writeln_fn  := standard_message out_stream true "D";
+    Output.tracing_fn  := standard_message out_stream true "E";
+    Output.warning_fn  := standard_message out_stream true "F";
+    Output.error_fn    := standard_message out_stream true "G";
+    Output.debug_fn    := standard_message out_stream true "H";
     Output.priority_fn := ! Output.writeln_fn;
     Output.prompt_fn   := ignore;
     (in_stream, out_stream)