# HG changeset patch
# User wenzelm
# Date 1284749792 -7200
# Node ID cab2719398a75b3837731685c6ad520ef2ef3abb
# Parent  dfacdb01e1ece096cd65ba2331b28cc74bf09242
Isabelle_Process: status/report do not require serial numbers;

diff -r dfacdb01e1ec -r cab2719398a7 src/Pure/System/isabelle_process.ML
--- 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)