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:
authorwenzelm
Sun Aug 22 22:28:24 2010 +0200 (2010-08-22)
changeset 385849f63135f3cbb
parent 38583 ff7f9510b0d6
child 38633 39412530436f
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") *}
src/Pure/PIDE/markup_tree.scala
     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!?