# HG changeset patch
# User wenzelm
# Date 1282297653 -7200
# Node ID 8176107637ceb217c02f1615a25bf9c5a3a2912a
# Parent  32b924a832c4829cc779788284a0e6b2026d9a0c
Branches.overlapping: proper treatment of stop_range that overlaps with end;
Markup_Tree.select: allow singularity in parent range specification;

diff -r 32b924a832c4 -r 8176107637ce src/Pure/PIDE/markup_tree.scala
--- a/src/Pure/PIDE/markup_tree.scala	Fri Aug 20 11:00:15 2010 +0200
+++ b/src/Pure/PIDE/markup_tree.scala	Fri Aug 20 11:47:33 2010 +0200
@@ -24,7 +24,7 @@
   }
 
 
-  /* branches sorted by quasi-order -- overlapping intervals appear as equivalent */
+  /* branches sorted by quasi-order -- overlapping ranges appear as equivalent */
 
   object Branches
   {
@@ -39,7 +39,15 @@
     def update(branches: T, entry: Entry): T = branches + (entry._1 -> entry)
 
     def overlapping(range: Text.Range, branches: T): T =
-      branches.range(Node(range.start_range, Nil), Node(range.stop_range, Nil))
+    {
+      val start = Node[Any](range.start_range, Nil)
+      val stop = Node[Any](range.stop_range, Nil)
+      branches.get(stop) match {
+        case Some(end) if range overlaps end._1.range =>
+          update(branches.range(start, stop), end)
+        case _ => branches.range(start, stop)
+      }
+    }
   }
 
   val empty = new Markup_Tree(Branches.empty)
@@ -131,7 +139,8 @@
               Stream(parent.restrict(Text.Range(last, parent.range.stop)))
             else Stream.Empty
         }
-      padding(parent.range.start, substream)
+      if (substream.isEmpty) Stream(parent)
+      else padding(parent.range.start, substream)
     }
     stream(Node(range, Nil), branches)
   }