src/Pure/PIDE/protocol.scala
changeset 55431 e0f20a44ff9d
parent 55429 4a50f9e70dc1
child 55432 9c53198dbb1c
     1.1 --- a/src/Pure/PIDE/protocol.scala	Tue Feb 11 15:55:05 2014 +0100
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Tue Feb 11 17:44:29 2014 +0100
     1.3 @@ -274,22 +274,25 @@
     1.4  
     1.5    private val include_pos = Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
     1.6  
     1.7 -  def message_positions(command: Command, message: XML.Elem): Set[Text.Range] =
     1.8 +  def message_positions(command_id: Document_ID.Command, chunk: Command.Chunk, message: XML.Elem)
     1.9 +    : Set[Text.Range] =
    1.10    {
    1.11      def elem_positions(raw_range: Text.Range, set: Set[Text.Range], body: XML.Body)
    1.12        : Set[Text.Range] =
    1.13      {
    1.14 -      val range = command.decode(raw_range).restrict(command.range)
    1.15 +      val range = chunk.decode(raw_range).restrict(chunk.range)
    1.16        body.foldLeft(if (range.is_singularity) set else set + range)(positions)
    1.17      }
    1.18  
    1.19      def positions(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] =
    1.20        tree match {
    1.21 -        case XML.Wrapped_Elem(Markup(name, Position.Reported(id, file, range)), _, body)
    1.22 -        if include_pos(name) && id == command.id && file == "" => elem_positions(range, set, body)
    1.23 +        case XML.Wrapped_Elem(Markup(name, Position.Reported(id, file_name, range)), _, body)
    1.24 +        if include_pos(name) && id == command_id && file_name == chunk.file_name =>
    1.25 +        elem_positions(range, set, body)
    1.26  
    1.27 -        case XML.Elem(Markup(name, Position.Reported(id, file, range)), body)
    1.28 -        if include_pos(name) && id == command.id && file == "" => elem_positions(range, set, body)
    1.29 +        case XML.Elem(Markup(name, Position.Reported(id, file_name, range)), body)
    1.30 +        if include_pos(name) && id == command_id && file_name == chunk.file_name =>
    1.31 +        elem_positions(range, set, body)
    1.32  
    1.33          case XML.Wrapped_Elem(_, _, body) => body.foldLeft(set)(positions)
    1.34  
    1.35 @@ -300,7 +303,7 @@
    1.36  
    1.37      val set = positions(Set.empty, message)
    1.38      if (set.isEmpty)
    1.39 -      set ++ Position.Range.unapply(message.markup.properties).map(command.decode(_))
    1.40 +      set ++ Position.Range.unapply(message.markup.properties).map(chunk.decode(_))
    1.41      else set
    1.42    }
    1.43  }
    1.44 @@ -323,7 +326,7 @@
    1.45        val encode_blob: T[Command.Blob] =
    1.46          variant(List(
    1.47            { case Exn.Res((a, b)) =>
    1.48 -              (Nil, pair(string, option(string))((a.node, b.map(_.toString)))) },
    1.49 +              (Nil, pair(string, option(string))((a.node, b.map(p => p._1.toString)))) },
    1.50            { case Exn.Exn(e) => (Nil, string(Exn.message(e))) }))
    1.51        YXML.string_of_body(list(encode_blob)(command.blobs))
    1.52      }