# HG changeset patch
# User wenzelm
# Date 1348334584 -7200
# Node ID b96e4a39cc3e01bc826790b7e341c1fcb9e2b5b6
# Parent  6d1465c00f2e1f2b3f8c6ca774cbe66add424189
accumulate under exec_id as well;

diff -r 6d1465c00f2e -r b96e4a39cc3e src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Sat Sep 22 19:16:48 2012 +0200
+++ b/src/Pure/PIDE/command.scala	Sat Sep 22 19:23:04 2012 +0200
@@ -28,7 +28,7 @@
     private def add_status(st: Markup): State = copy(status = st :: status)
     private def add_markup(m: Text.Markup): State = copy(markup = markup + m)
 
-    def + (message: XML.Elem): Command.State =
+    def + (alt_id: Document.ID, message: XML.Elem): Command.State =
       message match {
         case XML.Elem(Markup(Isabelle_Markup.STATUS, _), msgs) =>
           (this /: msgs)((state, msg) =>
@@ -43,7 +43,8 @@
           (this /: msgs)((state, msg) =>
             msg match {
               case XML.Elem(Markup(name, atts @ Position.Id_Range(id, raw_range)), args)
-              if id == command.id && command.range.contains(command.decode(raw_range)) =>
+              if (id == command.id || id == alt_id) &&
+                  command.range.contains(command.decode(raw_range)) =>
                 val range = command.decode(raw_range)
                 val props = Position.purge(atts)
                 val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
diff -r 6d1465c00f2e -r b96e4a39cc3e src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sat Sep 22 19:16:48 2012 +0200
+++ b/src/Pure/PIDE/document.scala	Sat Sep 22 19:23:04 2012 +0200
@@ -373,12 +373,12 @@
     def accumulate(id: ID, message: XML.Elem): (Command.State, State) =
       execs.get(id) match {
         case Some(st) =>
-          val new_st = st + message
+          val new_st = st + (id, message)
           (new_st, copy(execs = execs + (id -> new_st)))
         case None =>
           commands.get(id) match {
             case Some(st) =>
-              val new_st = st + message
+              val new_st = st + (id, message)
               (new_st, copy(commands = commands + (id -> new_st)))
             case None => fail
           }