# HG changeset patch
# User wenzelm
# Date 1408540352 -7200
# Node ID 2777096e0adf46304b3eace3ef5bca70e4f080c7
# Parent  47ecbef7274bd4f79957561e810f078ae9f731e2
default command position is only valid for default text chunk (amending dcb758188aa6);

diff -r 47ecbef7274b -r 2777096e0adf src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Wed Aug 20 11:54:17 2014 +0200
+++ b/src/Pure/PIDE/protocol.scala	Wed Aug 20 15:12:32 2014 +0200
@@ -320,7 +320,13 @@
     def elem_positions(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] =
       props match {
         case Position.Identified(id, name) if self_id(id) && name == chunk_name =>
-          Position.Range.unapply(props) orElse Position.Range.unapply(command_position) match {
+          val opt_range =
+            Position.Range.unapply(props) orElse {
+              if (name == Symbol.Text_Chunk.Default)
+                Position.Range.unapply(command_position)
+              else None
+            }
+          opt_range match {
             case Some(symbol_range) =>
               chunk.incorporate(symbol_range) match {
                 case Some(range) => set + range