diff -r afc7f88370a8 -r b610c0d52bfa src/Pure/PIDE/markup_tree.scala
--- a/src/Pure/PIDE/markup_tree.scala	Thu Sep 27 10:59:10 2012 +0200
+++ b/src/Pure/PIDE/markup_tree.scala	Thu Sep 27 14:46:34 2012 +0200
@@ -110,7 +110,6 @@
     val start = Text.Range(range.start)
     val stop = Text.Range(range.stop)
     val bs = branches.range(start, stop)
-    // FIXME check after Scala 2.8.x
     branches.get(stop) match {
       case Some(end) if range overlaps end.range => bs + (end.range -> end)
       case _ => bs
@@ -132,14 +131,8 @@
           new Markup_Tree(Branches.empty, Entry(new_markup, this))
         else {
           val body = overlapping(new_range)
-          if (body.forall(e => new_range.contains(e._1))) {
-            val rest = // branches -- body, modulo workarounds for Redblack in Scala 2.8.0 FIXME
-              if (body.size > 1)
-                (Branches.empty /: branches)((rest, entry) =>
-                  if (body.isDefinedAt(entry._1)) rest else rest + entry)
-              else branches
-            new Markup_Tree(rest, Entry(new_markup, new Markup_Tree(body)))
-          }
+          if (body.forall(e => new_range.contains(e._1)))
+            new Markup_Tree(branches -- body.keys, Entry(new_markup, new Markup_Tree(body)))
           else { // FIXME split markup!?
             System.err.println("Ignored overlapping markup information: " + new_markup +
               body.filter(e => !new_range.contains(e._1)).mkString("\n"))