1.1 --- a/src/Pure/PIDE/markup_tree.scala	Thu Aug 26 11:29:43 2010 +0200
     1.2 +++ b/src/Pure/PIDE/markup_tree.scala	Thu Aug 26 11:31:21 2010 +0200
     1.3 @@ -115,7 +115,10 @@
     1.4            if (last < stop) parent.restrict(Text.Range(last, stop)) #:: nexts
     1.5            else nexts
     1.6  
     1.7 -        case Nil => Stream(Text.Info(Text.Range(last, root_range.stop), default))
     1.8 +        case Nil =>
     1.9 +          val stop = root_range.stop
    1.10 +          if (last < stop) Stream(Text.Info(Text.Range(last, stop), default))
    1.11 +          else Stream.empty
    1.12        }
    1.13      }
    1.14      stream(root_range.start, List((Text.Info(root_range, default), overlapping(root_range))))