diff -r ae33d153f6cc -r b64b0cb845fe src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Tue Apr 08 10:24:42 2014 +0200 +++ b/src/Pure/PIDE/protocol.scala Tue Apr 08 12:19:33 2014 +0200 @@ -307,8 +307,8 @@ { def elem_positions(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] = props match { - case Position.Reported(id, file_name, symbol_range) - if valid_id(id) && file_name == chunk.file_name => + case Position.Reported(id, chunk_name, symbol_range) + if valid_id(id) && chunk_name == chunk.name => chunk.incorporate(symbol_range) match { case Some(range) => set + range case _ => set