src/Pure/PIDE/markup_tree.scala
changeset 49608 ce1c34c98eeb
parent 49607 b610c0d52bfa
child 49614 0009a6ebc83b
     1.1 --- a/src/Pure/PIDE/markup_tree.scala	Thu Sep 27 14:46:34 2012 +0200
     1.2 +++ b/src/Pure/PIDE/markup_tree.scala	Thu Sep 27 14:50:06 2012 +0200
     1.3 @@ -133,8 +133,8 @@
     1.4            val body = overlapping(new_range)
     1.5            if (body.forall(e => new_range.contains(e._1)))
     1.6              new Markup_Tree(branches -- body.keys, Entry(new_markup, new Markup_Tree(body)))
     1.7 -          else { // FIXME split markup!?
     1.8 -            System.err.println("Ignored overlapping markup information: " + new_markup +
     1.9 +          else {
    1.10 +            java.lang.System.err.println("Ignored overlapping markup information: " + new_markup +
    1.11                body.filter(e => !new_range.contains(e._1)).mkString("\n"))
    1.12              this
    1.13            }