src/Pure/PIDE/protocol.scala
changeset 56462 b64b0cb845fe
parent 56458 a8d960baa5c2
child 56468 30128d1acfbc
     1.1 --- a/src/Pure/PIDE/protocol.scala	Tue Apr 08 10:24:42 2014 +0200
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Tue Apr 08 12:19:33 2014 +0200
     1.3 @@ -307,8 +307,8 @@
     1.4    {
     1.5      def elem_positions(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] =
     1.6        props match {
     1.7 -        case Position.Reported(id, file_name, symbol_range)
     1.8 -        if valid_id(id) && file_name == chunk.file_name =>
     1.9 +        case Position.Reported(id, chunk_name, symbol_range)
    1.10 +        if valid_id(id) && chunk_name == chunk.name =>
    1.11            chunk.incorporate(symbol_range) match {
    1.12              case Some(range) => set + range
    1.13              case _ => set