src/Pure/PIDE/markup_tree.scala
changeset 38657 2e0ebdaac59b
parent 38584 9f63135f3cbb
child 38659 afac51977705
     1.1 --- a/src/Pure/PIDE/markup_tree.scala	Mon Aug 23 19:35:57 2010 +0200
     1.2 +++ b/src/Pure/PIDE/markup_tree.scala	Mon Aug 23 20:50:00 2010 +0200
     1.3 @@ -30,6 +30,7 @@
     1.4        })
     1.5  
     1.6      def update(branches: T, entry: Entry): T = branches + (entry._1.range -> entry)
     1.7 +    def single(entry: Entry): T = update(empty, entry)
     1.8  
     1.9      def overlapping(range: Text.Range, branches: T): T =
    1.10      {
    1.11 @@ -65,15 +66,21 @@
    1.12          new Markup_Tree(Branches.update(branches, new_info -> empty))
    1.13        case Some((info, subtree)) =>
    1.14          val range = info.range
    1.15 -        if (range != new_range && range.contains(new_range))
    1.16 +        if (range == new_range)
    1.17 +          new Markup_Tree(Branches.update(branches,
    1.18 +            new_info -> new Markup_Tree(Branches.single((info, subtree)))))
    1.19 +        else if (range.contains(new_range))
    1.20            new Markup_Tree(Branches.update(branches, info -> (subtree + new_info)))
    1.21          else if (new_range.contains(branches.head._1) && new_range.contains(branches.last._1))
    1.22 -          new Markup_Tree(Branches.update(Branches.empty, (new_info -> this)))
    1.23 +          new Markup_Tree(Branches.single(new_info -> this))
    1.24          else {
    1.25            val body = Branches.overlapping(new_range, branches)
    1.26            if (body.forall(e => new_range.contains(e._1))) {
    1.27 -            val rest = (Branches.empty /: branches)((rest, entry) =>
    1.28 -              if (body.isDefinedAt(entry._1)) rest else rest + entry)
    1.29 +            val rest = // branches -- body, with workarounds for Redblack in Scala 2.8.0
    1.30 +              if (body.size > 1)
    1.31 +                (Branches.empty /: branches)((rest, entry) =>
    1.32 +                  if (body.isDefinedAt(entry._1)) rest else rest + entry)
    1.33 +              else branches
    1.34              new Markup_Tree(Branches.update(rest, new_info -> new Markup_Tree(body)))
    1.35            }
    1.36            else { // FIXME split markup!?