1.1 --- a/src/Pure/PIDE/protocol.scala	Tue Aug 12 14:15:58 2014 +0200
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Tue Aug 12 15:31:24 2014 +0200
     1.3 @@ -312,17 +312,21 @@
     1.4  
     1.5    def message_positions(
     1.6      self_id: Document_ID.Generic => Boolean,
     1.7 +    command_position: Position.T,
     1.8      chunk_name: Symbol.Text_Chunk.Name,
     1.9      chunk: Symbol.Text_Chunk,
    1.10      message: XML.Elem): Set[Text.Range] =
    1.11    {
    1.12      def elem_positions(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] =
    1.13        props match {
    1.14 -        case Position.Reported(id, name, symbol_range)
    1.15 -        if self_id(id) && name == chunk_name =>
    1.16 -          chunk.incorporate(symbol_range) match {
    1.17 -            case Some(range) => set + range
    1.18 -            case _ => set
    1.19 +        case Position.Identified(id, name) if self_id(id) && name == chunk_name =>
    1.20 +          Position.Range.unapply(props) orElse Position.Range.unapply(command_position) match {
    1.21 +            case Some(symbol_range) =>
    1.22 +              chunk.incorporate(symbol_range) match {
    1.23 +                case Some(range) => set + range
    1.24 +                case _ => set
    1.25 +              }
    1.26 +            case None => set
    1.27            }
    1.28          case _ => set
    1.29        }