updated to consolidated SortedMap in scala-2.9.x;
authorwenzelm
Thu Sep 27 14:46:34 2012 +0200 (2012-09-27)
changeset 49607b610c0d52bfa
parent 49606 afc7f88370a8
child 49608 ce1c34c98eeb
updated to consolidated SortedMap in scala-2.9.x;
src/Pure/PIDE/markup_tree.scala
     1.1 --- a/src/Pure/PIDE/markup_tree.scala	Thu Sep 27 10:59:10 2012 +0200
     1.2 +++ b/src/Pure/PIDE/markup_tree.scala	Thu Sep 27 14:46:34 2012 +0200
     1.3 @@ -110,7 +110,6 @@
     1.4      val start = Text.Range(range.start)
     1.5      val stop = Text.Range(range.stop)
     1.6      val bs = branches.range(start, stop)
     1.7 -    // FIXME check after Scala 2.8.x
     1.8      branches.get(stop) match {
     1.9        case Some(end) if range overlaps end.range => bs + (end.range -> end)
    1.10        case _ => bs
    1.11 @@ -132,14 +131,8 @@
    1.12            new Markup_Tree(Branches.empty, Entry(new_markup, this))
    1.13          else {
    1.14            val body = overlapping(new_range)
    1.15 -          if (body.forall(e => new_range.contains(e._1))) {
    1.16 -            val rest = // branches -- body, modulo workarounds for Redblack in Scala 2.8.0 FIXME
    1.17 -              if (body.size > 1)
    1.18 -                (Branches.empty /: branches)((rest, entry) =>
    1.19 -                  if (body.isDefinedAt(entry._1)) rest else rest + entry)
    1.20 -              else branches
    1.21 -            new Markup_Tree(rest, Entry(new_markup, new Markup_Tree(body)))
    1.22 -          }
    1.23 +          if (body.forall(e => new_range.contains(e._1)))
    1.24 +            new Markup_Tree(branches -- body.keys, Entry(new_markup, new Markup_Tree(body)))
    1.25            else { // FIXME split markup!?
    1.26              System.err.println("Ignored overlapping markup information: " + new_markup +
    1.27                body.filter(e => !new_range.contains(e._1)).mkString("\n"))