accumulate only local results -- no proper history support yet;

--- a/src/Pure/PIDE/command.scala	Fri May 28 21:40:32 2010 +0200
+++ b/src/Pure/PIDE/command.scala	Fri May 28 22:21:08 2010 +0200
@@ -73,7 +73,7 @@
       react {
         case Consume(message, forward) if !assigned =>
           val old_state = state
-          state = old_state + message
+          state = old_state.accumulate(message)
           if (!(state eq old_state)) forward(static_parent getOrElse this)
 
         case Assign =>

--- a/src/Pure/PIDE/state.scala	Fri May 28 21:40:32 2010 +0200
+++ b/src/Pure/PIDE/state.scala	Fri May 28 22:21:08 2010 +0200
@@ -70,7 +70,7 @@
 
   /* message dispatch */
 
-  def + (message: XML.Tree): State =
+  def accumulate(message: XML.Tree): State =
     message match {
       case XML.Elem(Markup.STATUS, _, elems) =>
         (this /: elems)((state, elem) =>
@@ -78,7 +78,7 @@
             case XML.Elem(Markup.UNPROCESSED, _, _) => state.set_status(Command.Status.UNPROCESSED)
             case XML.Elem(Markup.FINISHED, _, _) => state.set_status(Command.Status.FINISHED)
             case XML.Elem(Markup.FAILED, _, _) => state.set_status(Command.Status.FAILED)
-            case XML.Elem(kind, atts, body) =>
+            case XML.Elem(kind, atts, body) if Position.get_id(atts) == Some(command.id) =>
               atts match {
                 case Position.Range(begin, end) =>
                   if (kind == Markup.ML_TYPING) {
@@ -99,11 +99,6 @@
                       case _ => state
                     }
                   }
-                  else if (kind == Markup.FACT_DECL || kind == Markup.LOCAL_FACT_DECL ||
-                      kind == Markup.ATTRIBUTE || kind == Markup.FIXED_DECL) {
-                    // FIXME usually displaced due to lack of full history support
-                    state
-                  }
                   else {
                     state.add_markup(
                       command.markup_node(begin - 1, end - 1, Command.HighlightInfo(kind)))