message serial number indicates physical order;

--- a/src/Pure/General/markup.ML	Mon Aug 30 11:17:05 2010 +0200
+++ b/src/Pure/General/markup.ML	Mon Aug 30 11:35:17 2010 +0200
@@ -115,6 +115,7 @@
   val assignN: string val assign: int -> T
   val editN: string val edit: int -> int -> T
   val pidN: string
+  val serialN: string
   val promptN: string val prompt: T
   val readyN: string val ready: T
   val no_output: output * output
@@ -337,6 +338,7 @@
 (* messages *)
 
 val pidN = "pid";
+val serialN = "serial";
 
 val (promptN, prompt) = markup_elem "prompt";
 val (readyN, ready) = markup_elem "ready";

--- a/src/Pure/General/markup.scala	Mon Aug 30 11:17:05 2010 +0200
+++ b/src/Pure/General/markup.scala	Mon Aug 30 11:35:17 2010 +0200
@@ -226,6 +226,7 @@
   /* messages */
 
   val PID = "pid"
+  val SERIAL = "serial"
 
   val MESSAGE = "message"
   val CLASS = "class"

--- a/src/Pure/System/isabelle_process.ML	Mon Aug 30 11:17:05 2010 +0200
+++ b/src/Pure/System/isabelle_process.ML	Mon Aug 30 11:35:17 2010 +0200
@@ -63,7 +63,8 @@
 in
 
 fun standard_message out_stream ch body =
-  message out_stream ch (Position.properties_of (Position.thread_data ())) body;
+  message out_stream ch
+    ((Markup.serialN, serial_string ()) :: Position.properties_of (Position.thread_data ())) body;
 
 fun init_message out_stream =
   message out_stream "A" [(Markup.pidN, process_id ())] (Session.welcome ());