src/Pure/PIDE/protocol.scala
changeset 56469 ffc94a271633
parent 56468 30128d1acfbc
child 56470 8eda56033203
     1.1 --- a/src/Pure/PIDE/protocol.scala	Tue Apr 08 15:12:54 2014 +0200
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Tue Apr 08 16:07:02 2014 +0200
     1.3 @@ -302,13 +302,14 @@
     1.4  
     1.5    def message_positions(
     1.6      valid_id: Document_ID.Generic => Boolean,
     1.7 +    chunk_name: Text.Chunk.Name,
     1.8      chunk: Text.Chunk,
     1.9      message: XML.Elem): Set[Text.Range] =
    1.10    {
    1.11      def elem_positions(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] =
    1.12        props match {
    1.13 -        case Position.Reported(id, chunk_name, symbol_range)
    1.14 -        if valid_id(id) && chunk_name == chunk.name =>
    1.15 +        case Position.Reported(id, name, symbol_range)
    1.16 +        if valid_id(id) && name == chunk_name =>
    1.17            chunk.incorporate(symbol_range) match {
    1.18              case Some(range) => set + range
    1.19              case _ => set