# HG changeset patch
# User wenzelm
# Date 1282753144 -7200
# Node ID 31da698fc4e578fd573f0191d88e8cbb1b130a12
# Parent  29d0298439bee55660e7cb734df838a24994508e
more precise Command.State accumulation;

diff -r 29d0298439be -r 31da698fc4e5 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Wed Aug 25 17:45:35 2010 +0200
+++ b/src/Pure/PIDE/command.scala	Wed Aug 25 18:19:04 2010 +0200
@@ -22,10 +22,10 @@
 
     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_markup(info: Text.Info[Any]): State = copy(markup = markup + info)
-
     def root_info: Text.Info[Any] =
       new Text.Info(command.range,
         XML.Elem(Markup(Markup.STATUS, Nil), status.reverse.map(XML.Elem(_, Nil))))
@@ -36,8 +36,12 @@
 
     def accumulate(message: XML.Tree): Command.State =
       message match {
-        case XML.Elem(Markup(Markup.STATUS, _), body) =>  // FIXME explicit body check!?
-          copy(status = (for (XML.Elem(markup, _) <- body) yield markup) ::: status)
+        case XML.Elem(Markup(Markup.STATUS, _), msgs) =>
+          (this /: msgs)((state, msg) =>
+            msg match {
+              case XML.Elem(markup, Nil) => state.add_status(markup)
+              case _ => System.err.println("Ignored status message: " + msg); state
+            })
 
         case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
           (this /: msgs)((state, msg) =>
@@ -47,7 +51,7 @@
                 val range = command.decode(Position.get_range(atts).get)
                 val props = atts.filterNot(p => Markup.POSITION_PROPERTIES(p._1))
                 val info = Text.Info[Any](range, XML.Elem(Markup(name, props), args))
-                add_markup(info)
+                state.add_markup(info)
               case _ => System.err.println("Ignored report message: " + msg); state
             })
         case _ => add_result(message)