tuned Markup_Tree.+ : slightly more expensive version to rebuild rest avoids crash of RedBlack.scala:120 (version Scala 2.8.0), e.g. on the following input:
ML {* fun f x = (x + 1, "aaa") *}

--- a/src/Pure/PIDE/markup_tree.scala	Sun Aug 22 22:09:14 2010 +0200
+++ b/src/Pure/PIDE/markup_tree.scala	Sun Aug 22 22:28:24 2010 +0200
@@ -72,7 +72,8 @@
         else {
           val body = Branches.overlapping(new_range, branches)
           if (body.forall(e => new_range.contains(e._1))) {
-            val rest = (branches /: body) { case (bs, (e, _)) => bs - e }
+            val rest = (Branches.empty /: branches)((rest, entry) =>
+              if (body.isDefinedAt(entry._1)) rest else rest + entry)
             new Markup_Tree(Branches.update(rest, new_info -> new Markup_Tree(body)))
           }
           else { // FIXME split markup!?