# HG changeset patch
# User wenzelm
# Date 1395859336 -3600
# Node ID a40e67ce4f8490fb8a2428fbefbd9c219ee0c271
# Parent  85911b8a6868c1111294b3aa436cc61d3efa8fb0
clarified valid_id: always standardize towards static command.id;

diff -r 85911b8a6868 -r a40e67ce4f84 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Wed Mar 26 14:41:52 2014 +0100
+++ b/src/Pure/PIDE/command.scala	Wed Mar 26 19:42:16 2014 +0100
@@ -132,7 +132,7 @@
       copy(markups = markups1.add(Markup_Index(false, file_name), m))
     }
 
-    def + (alt_id: Document_ID.Generic, message: XML.Elem): State =
+    def + (valid_id: Document_ID.Generic => Boolean, message: XML.Elem): State =
       message match {
         case XML.Elem(Markup(Markup.STATUS, _), msgs) =>
           (this /: msgs)((state, msg) =>
@@ -154,7 +154,7 @@
               msg match {
                 case XML.Elem(Markup(name,
                   atts @ Position.Reported(id, file_name, symbol_range)), args)
-                if id == command.id || id == alt_id =>
+                if valid_id(id) =>
                   command.chunks.get(file_name) match {
                     case Some(chunk) =>
                       chunk.incorporate(symbol_range) match {
@@ -187,7 +187,7 @@
               if (Protocol.is_inlined(message)) {
                 for {
                   (file_name, chunk) <- command.chunks
-                  range <- Protocol.message_positions(command.id, alt_id, chunk, message)
+                  range <- Protocol.message_positions(valid_id, chunk, message)
                 } st = st.add_markup(false, file_name, Text.Info(range, message2))
               }
               st
@@ -196,7 +196,7 @@
               System.err.println("Ignored message without serial number: " + message)
               this
           }
-      }
+    }
 
     def ++ (other: State): State =
       copy(
diff -r 85911b8a6868 -r a40e67ce4f84 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Wed Mar 26 14:41:52 2014 +0100
+++ b/src/Pure/PIDE/document.scala	Wed Mar 26 19:42:16 2014 +0100
@@ -521,15 +521,19 @@
     def the_dynamic_state(id: Document_ID.Exec): Command.State = execs.getOrElse(id, fail)
     def the_assignment(version: Version): State.Assignment = assignments.getOrElse(version.id, fail)
 
+    def valid_id(st: Command.State)(id: Document_ID.Generic): Boolean =
+      id == st.command.id ||
+      (execs.get(id) match { case Some(st1) => st1.command.id == st.command.id case None => false })
+
     def accumulate(id: Document_ID.Generic, message: XML.Elem): (Command.State, State) =
       execs.get(id) match {
         case Some(st) =>
-          val new_st = st + (id, message)
+          val new_st = st + (valid_id(st), message)
           (new_st, copy(execs = execs + (id -> new_st)))
         case None =>
           commands.get(id) match {
             case Some(st) =>
-              val new_st = st + (id, message)
+              val new_st = st + (valid_id(st), message)
               (new_st, copy(commands = commands + (id -> new_st)))
             case None => fail
           }
diff -r 85911b8a6868 -r a40e67ce4f84 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Wed Mar 26 14:41:52 2014 +0100
+++ b/src/Pure/PIDE/protocol.scala	Wed Mar 26 19:42:16 2014 +0100
@@ -280,15 +280,14 @@
     Document.Elements(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
 
   def message_positions(
-    command_id: Document_ID.Command,
-    alt_id: Document_ID.Generic,
+    valid_id: Document_ID.Generic => Boolean,
     chunk: Command.Chunk,
     message: XML.Elem): Set[Text.Range] =
   {
     def elem_positions(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] =
       props match {
         case Position.Reported(id, file_name, symbol_range)
-        if (id == command_id || id == alt_id) && file_name == chunk.file_name =>
+        if valid_id(id) && file_name == chunk.file_name =>
           chunk.incorporate(symbol_range) match {
             case Some(range) => set + range
             case _ => set