src/Pure/PIDE/command.scala
changeset 56470 8eda56033203
parent 56469 ffc94a271633
child 56473 5b5c750e9763
     1.1 --- a/src/Pure/PIDE/command.scala	Tue Apr 08 16:07:02 2014 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Tue Apr 08 19:17:28 2014 +0200
     1.3 @@ -81,6 +81,17 @@
     1.4      def add(index: Markup_Index, markup: Text.Markup): Markups =
     1.5        new Markups(rep + (index -> (this(index) + markup)))
     1.6  
     1.7 +    def other_id_iterator: Iterator[Document_ID.Generic] =
     1.8 +      for (Markup_Index(_, Text.Chunk.Id(other_id)) <- rep.keysIterator)
     1.9 +        yield other_id
    1.10 +
    1.11 +    def retarget(other_id: Document_ID.Generic): Markups =
    1.12 +      new Markups(
    1.13 +        (for {
    1.14 +          (Markup_Index(status, Text.Chunk.Id(id)), markup) <- rep.iterator
    1.15 +          if other_id == id
    1.16 +        } yield (Markup_Index(status, Text.Chunk.Default), markup)).toMap)
    1.17 +
    1.18      override def hashCode: Int = rep.hashCode
    1.19      override def equals(that: Any): Boolean =
    1.20        that match {
    1.21 @@ -124,6 +135,9 @@
    1.22  
    1.23      def markup(index: Markup_Index): Markup_Tree = markups(index)
    1.24  
    1.25 +    def retarget(other_command: Command): State =
    1.26 +      new State(other_command, Nil, Results.empty, markups.retarget(other_command.id))
    1.27 +
    1.28  
    1.29      def eq_content(other: State): Boolean =
    1.30        command.source == other.command.source &&
    1.31 @@ -143,7 +157,10 @@
    1.32        copy(markups = markups1.add(Markup_Index(false, chunk_name), m))
    1.33      }
    1.34  
    1.35 -    def + (valid_id: Document_ID.Generic => Boolean, message: XML.Elem): State =
    1.36 +    def accumulate(
    1.37 +        self_id: Document_ID.Generic => Boolean,
    1.38 +        other_id: Document_ID.Generic => Option[(Text.Chunk.Id, Text.Chunk)],
    1.39 +        message: XML.Elem): State =
    1.40        message match {
    1.41          case XML.Elem(Markup(Markup.STATUS, _), msgs) =>
    1.42            (this /: msgs)((state, msg) =>
    1.43 @@ -163,19 +180,25 @@
    1.44                def bad(): Unit = System.err.println("Ignored report message: " + msg)
    1.45  
    1.46                msg match {
    1.47 -                case XML.Elem(Markup(name,
    1.48 -                  atts @ Position.Reported(id, chunk_name, symbol_range)), args)
    1.49 -                if valid_id(id) =>
    1.50 -                  command.chunks.get(chunk_name) match {
    1.51 -                    case Some(chunk) =>
    1.52 -                      chunk.incorporate(symbol_range) match {
    1.53 +                case XML.Elem(
    1.54 +                    Markup(name, atts @ Position.Reported(id, chunk_name, symbol_range)), args) =>
    1.55 +
    1.56 +                  val target =
    1.57 +                    if (self_id(id) && command.chunks.isDefinedAt(chunk_name))
    1.58 +                      Some((chunk_name, command.chunks(chunk_name)))
    1.59 +                    else if (chunk_name == Text.Chunk.Default) other_id(id)
    1.60 +                    else None
    1.61 +
    1.62 +                  target match {
    1.63 +                    case Some((target_name, target_chunk)) =>
    1.64 +                      target_chunk.incorporate(symbol_range) match {
    1.65                          case Some(range) =>
    1.66                            val props = Position.purge(atts)
    1.67                            val info = Text.Info(range, XML.Elem(Markup(name, props), args))
    1.68 -                          state.add_markup(false, chunk_name, info)
    1.69 +                          state.add_markup(false, target_name, info)
    1.70                          case None => bad(); state
    1.71                        }
    1.72 -                    case None => bad(); state
    1.73 +                    case None => /* FIXME bad(); */ state
    1.74                    }
    1.75  
    1.76                  case XML.Elem(Markup(name, atts), args)
    1.77 @@ -185,7 +208,7 @@
    1.78                    val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
    1.79                    state.add_markup(false, Text.Chunk.Default, info)
    1.80  
    1.81 -                case _ => /* FIXME bad(); */ state
    1.82 +                case _ => bad(); state
    1.83                }
    1.84              })
    1.85          case XML.Elem(Markup(name, props), body) =>
    1.86 @@ -198,7 +221,7 @@
    1.87                if (Protocol.is_inlined(message)) {
    1.88                  for {
    1.89                    (chunk_name, chunk) <- command.chunks.iterator
    1.90 -                  range <- Protocol.message_positions(valid_id, chunk_name, chunk, message)
    1.91 +                  range <- Protocol.message_positions(self_id, chunk_name, chunk, message)
    1.92                  } st = st.add_markup(false, chunk_name, Text.Info(range, message2))
    1.93                }
    1.94                st