# HG changeset patch
# User wenzelm
# Date 1282508904 -7200
# Node ID 9f63135f3cbb4db3c4a2c9815de6497c08457baa
# Parent  ff7f9510b0d6a2cabe6855ce397e2a3a9c567e1a
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") *}

diff -r ff7f9510b0d6 -r 9f63135f3cbb src/Pure/PIDE/markup_tree.scala
--- 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!?