src/Pure/PIDE/markup_tree.scala
changeset 38584 9f63135f3cbb
parent 38582 3a6ce43d99b1
child 38657 2e0ebdaac59b
     1.1 --- a/src/Pure/PIDE/markup_tree.scala	Sun Aug 22 22:09:14 2010 +0200
     1.2 +++ b/src/Pure/PIDE/markup_tree.scala	Sun Aug 22 22:28:24 2010 +0200
     1.3 @@ -72,7 +72,8 @@
     1.4          else {
     1.5            val body = Branches.overlapping(new_range, branches)
     1.6            if (body.forall(e => new_range.contains(e._1))) {
     1.7 -            val rest = (branches /: body) { case (bs, (e, _)) => bs - e }
     1.8 +            val rest = (Branches.empty /: branches)((rest, entry) =>
     1.9 +              if (body.isDefinedAt(entry._1)) rest else rest + entry)
    1.10              new Markup_Tree(Branches.update(rest, new_info -> new Markup_Tree(body)))
    1.11            }
    1.12            else { // FIXME split markup!?