# HG changeset patch
# User wenzelm
# Date 1396977448 -7200
# Node ID 8eda560332036cb9c1c5842b638244368fe4f859
# Parent  ffc94a2716335b2462ed1ee519a8c32b7647d463
accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);

diff -r ffc94a271633 -r 8eda56033203 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Tue Apr 08 16:07:02 2014 +0200
+++ b/src/Pure/PIDE/command.scala	Tue Apr 08 19:17:28 2014 +0200
@@ -81,6 +81,17 @@
     def add(index: Markup_Index, markup: Text.Markup): Markups =
       new Markups(rep + (index -> (this(index) + markup)))
 
+    def other_id_iterator: Iterator[Document_ID.Generic] =
+      for (Markup_Index(_, Text.Chunk.Id(other_id)) <- rep.keysIterator)
+        yield other_id
+
+    def retarget(other_id: Document_ID.Generic): Markups =
+      new Markups(
+        (for {
+          (Markup_Index(status, Text.Chunk.Id(id)), markup) <- rep.iterator
+          if other_id == id
+        } yield (Markup_Index(status, Text.Chunk.Default), markup)).toMap)
+
     override def hashCode: Int = rep.hashCode
     override def equals(that: Any): Boolean =
       that match {
@@ -124,6 +135,9 @@
 
     def markup(index: Markup_Index): Markup_Tree = markups(index)
 
+    def retarget(other_command: Command): State =
+      new State(other_command, Nil, Results.empty, markups.retarget(other_command.id))
+
 
     def eq_content(other: State): Boolean =
       command.source == other.command.source &&
@@ -143,7 +157,10 @@
       copy(markups = markups1.add(Markup_Index(false, chunk_name), m))
     }
 
-    def + (valid_id: Document_ID.Generic => Boolean, message: XML.Elem): State =
+    def accumulate(
+        self_id: Document_ID.Generic => Boolean,
+        other_id: Document_ID.Generic => Option[(Text.Chunk.Id, Text.Chunk)],
+        message: XML.Elem): State =
       message match {
         case XML.Elem(Markup(Markup.STATUS, _), msgs) =>
           (this /: msgs)((state, msg) =>
@@ -163,19 +180,25 @@
               def bad(): Unit = System.err.println("Ignored report message: " + msg)
 
               msg match {
-                case XML.Elem(Markup(name,
-                  atts @ Position.Reported(id, chunk_name, symbol_range)), args)
-                if valid_id(id) =>
-                  command.chunks.get(chunk_name) match {
-                    case Some(chunk) =>
-                      chunk.incorporate(symbol_range) match {
+                case XML.Elem(
+                    Markup(name, atts @ Position.Reported(id, chunk_name, symbol_range)), args) =>
+
+                  val target =
+                    if (self_id(id) && command.chunks.isDefinedAt(chunk_name))
+                      Some((chunk_name, command.chunks(chunk_name)))
+                    else if (chunk_name == Text.Chunk.Default) other_id(id)
+                    else None
+
+                  target match {
+                    case Some((target_name, target_chunk)) =>
+                      target_chunk.incorporate(symbol_range) match {
                         case Some(range) =>
                           val props = Position.purge(atts)
                           val info = Text.Info(range, XML.Elem(Markup(name, props), args))
-                          state.add_markup(false, chunk_name, info)
+                          state.add_markup(false, target_name, info)
                         case None => bad(); state
                       }
-                    case None => bad(); state
+                    case None => /* FIXME bad(); */ state
                   }
 
                 case XML.Elem(Markup(name, atts), args)
@@ -185,7 +208,7 @@
                   val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
                   state.add_markup(false, Text.Chunk.Default, info)
 
-                case _ => /* FIXME bad(); */ state
+                case _ => bad(); state
               }
             })
         case XML.Elem(Markup(name, props), body) =>
@@ -198,7 +221,7 @@
               if (Protocol.is_inlined(message)) {
                 for {
                   (chunk_name, chunk) <- command.chunks.iterator
-                  range <- Protocol.message_positions(valid_id, chunk_name, chunk, message)
+                  range <- Protocol.message_positions(self_id, chunk_name, chunk, message)
                 } st = st.add_markup(false, chunk_name, Text.Info(range, message2))
               }
               st
diff -r ffc94a271633 -r 8eda56033203 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Tue Apr 08 16:07:02 2014 +0200
+++ b/src/Pure/PIDE/document.scala	Tue Apr 08 19:17:28 2014 +0200
@@ -483,11 +483,19 @@
   }
 
   final case class State private(
+    /*reachable versions*/
     val versions: Map[Document_ID.Version, Version] = Map.empty,
-    val blobs: Set[SHA1.Digest] = Set.empty,   // inlined files
-    val commands: Map[Document_ID.Command, Command.State] = Map.empty,  // static markup from define_command
-    val execs: Map[Document_ID.Exec, Command.State] = Map.empty,  // dynamic markup from execution
+    /*inlined auxiliary files*/
+    val blobs: Set[SHA1.Digest] = Set.empty,
+    /*static markup from define_command*/
+    val commands: Map[Document_ID.Command, Command.State] = Map.empty,
+    /*dynamic markup from execution*/
+    val execs: Map[Document_ID.Exec, Command.State] = Map.empty,
+    /*command-exec assignment for each version*/
     val assignments: Map[Document_ID.Version, State.Assignment] = Map.empty,
+    /*commands with markup produced by other commands (imm_succs)*/
+    val augmented_commands: Graph[Document_ID.Command, Unit] = Graph.long,
+    /*explicit (linear) history*/
     val history: History = History.init)
   {
     private def fail[A]: A = throw new State.Fail(this)
@@ -524,23 +532,35 @@
     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 =
+    private def self_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 })
 
+    private def other_id(id: Document_ID.Generic): Option[(Text.Chunk.Id, Text.Chunk)] =
+      (execs.get(id) orElse commands.get(id)).map(st =>
+        ((Text.Chunk.Id(st.command.id), st.command.chunk)))
+
+    private def augmented(st: Command.State): Graph[Document_ID.Command, Unit] =
+      (augmented_commands /: st.markups.other_id_iterator)({ case (graph, id) =>
+        graph.default_node(id, ()).default_node(st.command.id, ()).add_edge(id, st.command.id) })
+
     def accumulate(id: Document_ID.Generic, message: XML.Elem): (Command.State, State) =
+    {
       execs.get(id) match {
         case Some(st) =>
-          val new_st = st + (valid_id(st), message)
-          (new_st, copy(execs = execs + (id -> new_st)))
+          val new_st = st.accumulate(self_id(st), other_id _, message)
+          val execs1 = execs + (id -> new_st)
+          (new_st, copy(execs = execs1, augmented_commands = augmented(new_st)))
         case None =>
           commands.get(id) match {
             case Some(st) =>
-              val new_st = st + (valid_id(st), message)
-              (new_st, copy(commands = commands + (id -> new_st)))
+              val new_st = st.accumulate(self_id(st), other_id _, message)
+              val commands1 = commands + (id -> new_st)
+              (new_st, copy(commands = commands1, augmented_commands = augmented(new_st)))
             case None => fail
           }
       }
+    }
 
     def assign(id: Document_ID.Version, update: Assign_Update): (List[Command], State) =
     {
@@ -629,27 +649,48 @@
             execs.get(exec_id).foreach(st => execs1 += (exec_id -> st))
         }
       }
-      copy(versions = versions1, blobs = blobs1, commands = commands1, execs = execs1,
+      copy(
+        versions = versions1,
+        blobs = blobs1,
+        commands = commands1,
+        execs = execs1,
+        augmented_commands = augmented_commands.restrict(commands1.isDefinedAt(_)),
         assignments = assignments1)
     }
 
-    def command_states(version: Version, command: Command): List[Command.State] =
+    private def command_states_self(version: Version, command: Command)
+      : List[(Document_ID.Generic, Command.State)] =
     {
       require(is_assigned(version))
       try {
         the_assignment(version).check_finished.command_execs.getOrElse(command.id, Nil)
-          .map(the_dynamic_state(_)) match {
+          .map(id => id -> the_dynamic_state(id)) match {
             case Nil => fail
-            case states => states
+            case res => res
           }
       }
       catch {
         case _: State.Fail =>
-          try { List(the_static_state(command.id)) }
-          catch { case _: State.Fail => List(command.init_state) }
+          try { List(command.id -> the_static_state(command.id)) }
+          catch { case _: State.Fail => List(command.id -> command.init_state) }
       }
     }
 
+    def command_states(version: Version, command: Command): List[Command.State] =
+    {
+      val self = command_states_self(version, command)
+      val others =
+        if (augmented_commands.defined(command.id)) {
+          (for {
+            command_id <- augmented_commands.imm_succs(command.id).iterator
+            (id, st) <- command_states_self(version, the_static_state(command_id).command)
+            if !self.exists(_._1 == id)
+          } yield (id, st)).toMap.valuesIterator.toList
+        }
+        else Nil
+      self.map(_._2) ::: others.map(_.retarget(command))
+    }
+
     def command_results(version: Version, command: Command): Command.Results =
       Command.State.merge_results(command_states(version, command))
 
diff -r ffc94a271633 -r 8eda56033203 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Tue Apr 08 16:07:02 2014 +0200
+++ b/src/Pure/PIDE/protocol.scala	Tue Apr 08 19:17:28 2014 +0200
@@ -301,7 +301,7 @@
     Document.Elements(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
 
   def message_positions(
-    valid_id: Document_ID.Generic => Boolean,
+    self_id: Document_ID.Generic => Boolean,
     chunk_name: Text.Chunk.Name,
     chunk: Text.Chunk,
     message: XML.Elem): Set[Text.Range] =
@@ -309,7 +309,7 @@
     def elem_positions(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] =
       props match {
         case Position.Reported(id, name, symbol_range)
-        if valid_id(id) && name == chunk_name =>
+        if self_id(id) && name == chunk_name =>
           chunk.incorporate(symbol_range) match {
             case Some(range) => set + range
             case _ => set
diff -r ffc94a271633 -r 8eda56033203 src/Pure/PIDE/text.scala
--- a/src/Pure/PIDE/text.scala	Tue Apr 08 16:07:02 2014 +0200
+++ b/src/Pure/PIDE/text.scala	Tue Apr 08 19:17:28 2014 +0200
@@ -106,6 +106,7 @@
   {
     sealed abstract class Name
     case object Default extends Name
+    case class Id(id: Document_ID.Generic) extends Name
     case class File_Name(file_name: String) extends Name
 
     class File(text: CharSequence) extends Chunk