src/Pure/PIDE/protocol.scala
changeset 58015 2777096e0adf
parent 57916 2c2c24dbf0a4
child 59085 08a6901eb035
     1.1 --- a/src/Pure/PIDE/protocol.scala	Wed Aug 20 11:54:17 2014 +0200
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Wed Aug 20 15:12:32 2014 +0200
     1.3 @@ -320,7 +320,13 @@
     1.4      def elem_positions(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] =
     1.5        props match {
     1.6          case Position.Identified(id, name) if self_id(id) && name == chunk_name =>
     1.7 -          Position.Range.unapply(props) orElse Position.Range.unapply(command_position) match {
     1.8 +          val opt_range =
     1.9 +            Position.Range.unapply(props) orElse {
    1.10 +              if (name == Symbol.Text_Chunk.Default)
    1.11 +                Position.Range.unapply(command_position)
    1.12 +              else None
    1.13 +            }
    1.14 +          opt_range match {
    1.15              case Some(symbol_range) =>
    1.16                chunk.incorporate(symbol_range) match {
    1.17                  case Some(range) => set + range