default command position is only valid for default text chunk (amending dcb758188aa6);
authorwenzelm
Wed Aug 20 15:12:32 2014 +0200 (2014-08-20)
changeset 580152777096e0adf
parent 58014 47ecbef7274b
child 58016 28e5ccf4a27f
default command position is only valid for default text chunk (amending dcb758188aa6);
src/Pure/PIDE/protocol.scala
     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