Markup_Tree.select: uniform treatment of root_range wrt. singularities, yielding empty result stream;

--- 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))))