# HG changeset patch
# User wenzelm
# Date 1282815081 -7200
# Node ID 6d5f9af42eca42d3e5f594e03ad3e74f15415e2e
# Parent  3d9d5ff80f6f77c578085dc46b3707d351a501f5
Markup_Tree.select: uniform treatment of root_range wrt. singularities, yielding empty result stream;

diff -r 3d9d5ff80f6f -r 6d5f9af42eca src/Pure/PIDE/markup_tree.scala
--- a/src/Pure/PIDE/markup_tree.scala	Thu Aug 26 11:29:43 2010 +0200
+++ b/src/Pure/PIDE/markup_tree.scala	Thu Aug 26 11:31:21 2010 +0200
@@ -115,7 +115,10 @@
           if (last < stop) parent.restrict(Text.Range(last, stop)) #:: nexts
           else nexts
 
-        case Nil => Stream(Text.Info(Text.Range(last, root_range.stop), default))
+        case Nil =>
+          val stop = root_range.stop
+          if (last < stop) Stream(Text.Info(Text.Range(last, stop), default))
+          else Stream.empty
       }
     }
     stream(root_range.start, List((Text.Info(root_range, default), overlapping(root_range))))