src/Pure/PIDE/markup_tree.scala
changeset 55618 995162143ef4
parent 52900 d29bf6db8a2d
child 55620 19dffae33cde
     1.1 --- a/src/Pure/PIDE/markup_tree.scala	Thu Feb 20 14:17:28 2014 +0100
     1.2 +++ b/src/Pure/PIDE/markup_tree.scala	Thu Feb 20 14:36:17 2014 +0100
     1.3 @@ -176,7 +176,7 @@
     1.4            if (body.forall(e => new_range.contains(e._1)))
     1.5              new Markup_Tree(branches -- body.keys, Entry(new_markup, new Markup_Tree(body)))
     1.6            else {
     1.7 -            java.lang.System.err.println("Ignored overlapping markup information: " + new_markup +
     1.8 +            System.err.println("Ignored overlapping markup information: " + new_markup +
     1.9                body.filter(e => !new_range.contains(e._1)).mkString("\n"))
    1.10              this
    1.11            }