src/Pure/PIDE/protocol.scala
changeset 56470 8eda56033203
parent 56469 ffc94a271633
child 56474 4df2727a0b5f
     1.1 --- a/src/Pure/PIDE/protocol.scala	Tue Apr 08 16:07:02 2014 +0200
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Tue Apr 08 19:17:28 2014 +0200
     1.3 @@ -301,7 +301,7 @@
     1.4      Document.Elements(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
     1.5  
     1.6    def message_positions(
     1.7 -    valid_id: Document_ID.Generic => Boolean,
     1.8 +    self_id: Document_ID.Generic => Boolean,
     1.9      chunk_name: Text.Chunk.Name,
    1.10      chunk: Text.Chunk,
    1.11      message: XML.Elem): Set[Text.Range] =
    1.12 @@ -309,7 +309,7 @@
    1.13      def elem_positions(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] =
    1.14        props match {
    1.15          case Position.Reported(id, name, symbol_range)
    1.16 -        if valid_id(id) && name == chunk_name =>
    1.17 +        if self_id(id) && name == chunk_name =>
    1.18            chunk.incorporate(symbol_range) match {
    1.19              case Some(range) => set + range
    1.20              case _ => set