src/Pure/PIDE/protocol.scala
changeset 55432 9c53198dbb1c
parent 55431 e0f20a44ff9d
child 55433 d2960d67f163
     1.1 --- a/src/Pure/PIDE/protocol.scala	Tue Feb 11 17:44:29 2014 +0100
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Tue Feb 11 21:58:31 2014 +0100
     1.3 @@ -302,8 +302,14 @@
     1.4        }
     1.5  
     1.6      val set = positions(Set.empty, message)
     1.7 -    if (set.isEmpty)
     1.8 -      set ++ Position.Range.unapply(message.markup.properties).map(chunk.decode(_))
     1.9 +    if (set.isEmpty) {
    1.10 +      message.markup.properties match {
    1.11 +        case Position.Reported(id, file_name, range)
    1.12 +        if id == command_id && file_name == chunk.file_name =>
    1.13 +          set + chunk.decode(range)
    1.14 +        case _ => set
    1.15 +      }
    1.16 +    }
    1.17      else set
    1.18    }
    1.19  }