# HG changeset patch
# User wenzelm
# Date 1283160917 -7200
# Node ID 28496da3bec24b9208e51e198b3dbeefb1c0e0b3
# Parent  fb9f51ba1bbc856de70ce3141e80ca39c8a835a5
message serial number indicates physical order;

diff -r fb9f51ba1bbc -r 28496da3bec2 src/Pure/General/markup.ML
--- 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";
diff -r fb9f51ba1bbc -r 28496da3bec2 src/Pure/General/markup.scala
--- 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"
diff -r fb9f51ba1bbc -r 28496da3bec2 src/Pure/System/isabelle_process.ML
--- 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 ());