diff -r 6f50d445f0e3 -r f2c0eaedd579 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Mon Mar 03 12:24:14 2014 +0100
+++ b/src/Pure/PIDE/protocol.scala	Mon Mar 03 12:54:12 2014 +0100
@@ -287,9 +287,9 @@
   {
     def elem_positions(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] =
       props match {
-        case Position.Reported(id, file_name, raw_range)
+        case Position.Reported(id, file_name, symbol_range)
         if (id == command_id || id == alt_id) && file_name == chunk.file_name =>
-          chunk.incorporate(raw_range) match {
+          chunk.incorporate(symbol_range) match {
             case Some(range) => set + range
             case _ => set
           }