src/Pure/PIDE/protocol.scala
changeset 55884 f2c0eaedd579
parent 55822 ccf2d784be97
child 56295 a40e67ce4f84
     1.1 --- a/src/Pure/PIDE/protocol.scala	Mon Mar 03 12:24:14 2014 +0100
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Mon Mar 03 12:54:12 2014 +0100
     1.3 @@ -287,9 +287,9 @@
     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, raw_range)
     1.8 +        case Position.Reported(id, file_name, symbol_range)
     1.9          if (id == command_id || id == alt_id) && file_name == chunk.file_name =>
    1.10 -          chunk.incorporate(raw_range) match {
    1.11 +          chunk.incorporate(symbol_range) match {
    1.12              case Some(range) => set + range
    1.13              case _ => set
    1.14            }