Command.results: ordered by serial number;

--- a/src/Pure/General/markup.scala	Mon Aug 30 11:35:17 2010 +0200
+++ b/src/Pure/General/markup.scala	Mon Aug 30 13:01:32 2010 +0200
@@ -226,7 +226,7 @@
   /* messages */
 
   val PID = "pid"
-  val SERIAL = "serial"
+  val Serial = new Long_Property("serial")
 
   val MESSAGE = "message"
   val CLASS = "class"

--- a/src/Pure/General/position.scala	Mon Aug 30 11:35:17 2010 +0200
+++ b/src/Pure/General/position.scala	Mon Aug 30 13:01:32 2010 +0200
@@ -28,4 +28,6 @@
         case _ => None
       }
   }
+
+  def purge(props: T): T = props.filterNot(p => Markup.POSITION_PROPERTIES(p._1))
 }

--- a/src/Pure/PIDE/command.scala	Mon Aug 30 11:35:17 2010 +0200
+++ b/src/Pure/PIDE/command.scala	Mon Aug 30 13:01:32 2010 +0200
@@ -8,23 +8,25 @@
 package isabelle
 
 
+import scala.collection.immutable.SortedMap
+
+
 object Command
 {
   /** accumulated results from prover **/
 
   case class State(
     val command: Command,
-    val status: List[Markup],
-    val reverse_results: List[XML.Tree],
-    val markup: Markup_Tree)
+    val status: List[Markup] = Nil,
+    val results: SortedMap[Long, XML.Tree] = SortedMap.empty,
+    val markup: Markup_Tree = Markup_Tree.empty)
   {
     /* content */
 
-    lazy val results = reverse_results.reverse
-
     def add_status(st: Markup): State = copy(status = st :: status)
     def add_markup(info: Text.Info[Any]): State = copy(markup = markup + info)
-    def add_result(result: XML.Tree): State = copy(reverse_results = result :: reverse_results)
+    def add_result(serial: Long, result: XML.Tree): State =
+      copy(results = results + (serial -> result))
 
     def root_info: Text.Info[Any] =
       new Text.Info(command.range,
@@ -34,7 +36,7 @@
 
     /* message dispatch */
 
-    def accumulate(message: XML.Tree): Command.State =
+    def accumulate(message: XML.Elem): Command.State =
       message match {
         case XML.Elem(Markup(Markup.STATUS, _), msgs) =>
           (this /: msgs)((state, msg) =>
@@ -48,13 +50,18 @@
             msg match {
               case XML.Elem(Markup(name, atts @ Position.Range(range)), args)
               if Position.Id.unapply(atts) == Some(command.id) =>
-                val props = atts.filterNot(p => Markup.POSITION_PROPERTIES(p._1))
+                val props = Position.purge(atts)
                 val info =
                   Text.Info[Any](command.decode(range), XML.Elem(Markup(name, props), args))
                 state.add_markup(info)
               case _ => System.err.println("Ignored report message: " + msg); state
             })
-        case _ => add_result(message)
+        case XML.Elem(Markup(name, atts), body) =>
+          atts match {
+            case Markup.Serial(i) =>
+              add_result(i, XML.Elem(Markup(name, Position.purge(atts)), body))
+            case _ => System.err.println("Ignored message without serial number: " + message); this
+          }
       }
   }
 
@@ -98,5 +105,5 @@
 
   /* accumulated results */
 
-  val empty_state: Command.State = Command.State(this, Nil, Nil, Markup_Tree.empty)
+  val empty_state: Command.State = Command.State(this)
 }

--- a/src/Pure/PIDE/document.scala	Mon Aug 30 11:35:17 2010 +0200
+++ b/src/Pure/PIDE/document.scala	Mon Aug 30 13:01:32 2010 +0200
@@ -204,7 +204,7 @@
     def the_exec_state(id: Exec_ID): Command.State = execs.getOrElse(id, fail)._1
     def the_assignment(version: Version): State.Assignment = assignments.getOrElse(version, fail)
 
-    def accumulate(id: ID, message: XML.Tree): (Command.State, State) =
+    def accumulate(id: ID, message: XML.Elem): (Command.State, State) =
       execs.get(id) match {
         case Some((st, occs)) =>
           val new_st = st.accumulate(message)

--- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Mon Aug 30 11:35:17 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Mon Aug 30 13:01:32 2010 +0200
@@ -67,12 +67,12 @@
             case Some(cmd) if !restriction.isDefined || restriction.get.contains(cmd) =>
               val snapshot = doc_view.model.snapshot()
               val filtered_results =
-                snapshot.state(cmd).results filter {
+                snapshot.state(cmd).results.iterator.map(_._2) filter {
                   case XML.Elem(Markup(Markup.TRACING, _), _) => show_tracing
                   case XML.Elem(Markup(Markup.DEBUG, _), _) => show_debug
                   case _ => true
                 }
-              html_panel.render(filtered_results)
+              html_panel.render(filtered_results.toList)
             case _ =>
           }
         case None =>