src/Pure/PIDE/protocol.scala
changeset 56295 a40e67ce4f84
parent 55884 f2c0eaedd579
child 56299 8201790fdeb9
     1.1 --- a/src/Pure/PIDE/protocol.scala	Wed Mar 26 14:41:52 2014 +0100
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Wed Mar 26 19:42:16 2014 +0100
     1.3 @@ -280,15 +280,14 @@
     1.4      Document.Elements(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
     1.5  
     1.6    def message_positions(
     1.7 -    command_id: Document_ID.Command,
     1.8 -    alt_id: Document_ID.Generic,
     1.9 +    valid_id: Document_ID.Generic => Boolean,
    1.10      chunk: Command.Chunk,
    1.11      message: XML.Elem): Set[Text.Range] =
    1.12    {
    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, file_name, symbol_range)
    1.16 -        if (id == command_id || id == alt_id) && file_name == chunk.file_name =>
    1.17 +        if valid_id(id) && file_name == chunk.file_name =>
    1.18            chunk.incorporate(symbol_range) match {
    1.19              case Some(range) => set + range
    1.20              case _ => set