src/Pure/PIDE/markup_tree.scala
changeset 38566 8176107637ce
parent 38564 a6e2715fac5f
child 38568 f117ba49a59c
     1.1 --- a/src/Pure/PIDE/markup_tree.scala	Fri Aug 20 11:00:15 2010 +0200
     1.2 +++ b/src/Pure/PIDE/markup_tree.scala	Fri Aug 20 11:47:33 2010 +0200
     1.3 @@ -24,7 +24,7 @@
     1.4    }
     1.5  
     1.6  
     1.7 -  /* branches sorted by quasi-order -- overlapping intervals appear as equivalent */
     1.8 +  /* branches sorted by quasi-order -- overlapping ranges appear as equivalent */
     1.9  
    1.10    object Branches
    1.11    {
    1.12 @@ -39,7 +39,15 @@
    1.13      def update(branches: T, entry: Entry): T = branches + (entry._1 -> entry)
    1.14  
    1.15      def overlapping(range: Text.Range, branches: T): T =
    1.16 -      branches.range(Node(range.start_range, Nil), Node(range.stop_range, Nil))
    1.17 +    {
    1.18 +      val start = Node[Any](range.start_range, Nil)
    1.19 +      val stop = Node[Any](range.stop_range, Nil)
    1.20 +      branches.get(stop) match {
    1.21 +        case Some(end) if range overlaps end._1.range =>
    1.22 +          update(branches.range(start, stop), end)
    1.23 +        case _ => branches.range(start, stop)
    1.24 +      }
    1.25 +    }
    1.26    }
    1.27  
    1.28    val empty = new Markup_Tree(Branches.empty)
    1.29 @@ -131,7 +139,8 @@
    1.30                Stream(parent.restrict(Text.Range(last, parent.range.stop)))
    1.31              else Stream.Empty
    1.32          }
    1.33 -      padding(parent.range.start, substream)
    1.34 +      if (substream.isEmpty) Stream(parent)
    1.35 +      else padding(parent.range.start, substream)
    1.36      }
    1.37      stream(Node(range, Nil), branches)
    1.38    }