# HG changeset patch
# User wenzelm
# Date 1392198649 -3600
# Node ID d2960d67f163ac1ca6eee853714574ad76b3333d
# Parent  9c53198dbb1cbed289c61d4377362e156a75b4bf
clarified message_positions: cover alt_id as well;
tuned;

diff -r 9c53198dbb1c -r d2960d67f163 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Tue Feb 11 21:58:31 2014 +0100
+++ b/src/Pure/PIDE/command.scala	Wed Feb 12 10:50:49 2014 +0100
@@ -141,19 +141,14 @@
               val message1 = XML.Elem(Markup(Markup.message(name), props), body)
               val message2 = XML.Elem(Markup(name, props), body)
 
-              val st0 = copy(results = results + (i -> message1))
-              val st1 =
-                if (Protocol.is_inlined(message)) {
-                  var st1 = st0
-                  for {
-                    (file_name, chunk) <- command.chunks
-                    range <- Protocol.message_positions(command.id, chunk, message)
-                  } st1 = st1.add_markup(file_name, Text.Info(range, message2))
-                  st1
-                }
-                else st0
-
-              st1
+              var st = copy(results = results + (i -> message1))
+              if (Protocol.is_inlined(message)) {
+                for {
+                  (file_name, chunk) <- command.chunks
+                  range <- Protocol.message_positions(command.id, alt_id, chunk, message)
+                } st = st.add_markup(file_name, Text.Info(range, message2))
+              }
+              st
 
             case _ =>
               java.lang.System.err.println("Ignored message without serial number: " + message)
diff -r 9c53198dbb1c -r d2960d67f163 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Tue Feb 11 21:58:31 2014 +0100
+++ b/src/Pure/PIDE/protocol.scala	Wed Feb 12 10:50:49 2014 +0100
@@ -274,42 +274,32 @@
 
   private val include_pos = Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
 
-  def message_positions(command_id: Document_ID.Command, chunk: Command.Chunk, message: XML.Elem)
-    : Set[Text.Range] =
+  def message_positions(
+    command_id: Document_ID.Command,
+    alt_id: Document_ID.Generic,
+    chunk: Command.Chunk,
+    message: XML.Elem): Set[Text.Range] =
   {
-    def elem_positions(raw_range: Text.Range, set: Set[Text.Range], body: XML.Body)
-      : Set[Text.Range] =
-    {
-      val range = chunk.decode(raw_range).restrict(chunk.range)
-      body.foldLeft(if (range.is_singularity) set else set + range)(positions)
-    }
+    def elem_positions(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] =
+      props match {
+        case Position.Reported(id, file_name, range)
+        if (id == command_id || id == alt_id) && file_name == chunk.file_name =>
+          val range1 = chunk.decode(range).restrict(chunk.range)
+          if (range1.is_singularity) set else set + range1
+        case _ => set
+      }
 
     def positions(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] =
       tree match {
-        case XML.Wrapped_Elem(Markup(name, Position.Reported(id, file_name, range)), _, body)
-        if include_pos(name) && id == command_id && file_name == chunk.file_name =>
-        elem_positions(range, set, body)
-
-        case XML.Elem(Markup(name, Position.Reported(id, file_name, range)), body)
-        if include_pos(name) && id == command_id && file_name == chunk.file_name =>
-        elem_positions(range, set, body)
-
-        case XML.Wrapped_Elem(_, _, body) => body.foldLeft(set)(positions)
-
-        case XML.Elem(_, body) => body.foldLeft(set)(positions)
-
-        case _ => set
+        case XML.Wrapped_Elem(Markup(name, props), _, body) =>
+          body.foldLeft(if (include_pos(name)) elem_positions(props, set) else set)(positions)
+        case XML.Elem(Markup(name, props), body) =>
+          body.foldLeft(if (include_pos(name)) elem_positions(props, set) else set)(positions)
+        case XML.Text(_) => set
       }
 
     val set = positions(Set.empty, message)
-    if (set.isEmpty) {
-      message.markup.properties match {
-        case Position.Reported(id, file_name, range)
-        if id == command_id && file_name == chunk.file_name =>
-          set + chunk.decode(range)
-        case _ => set
-      }
-    }
+    if (set.isEmpty) elem_positions(message.markup.properties, set)
     else set
   }
 }