diff -r 2c585bb9560c -r 995162143ef4 src/Pure/PIDE/markup_tree.scala --- a/src/Pure/PIDE/markup_tree.scala Thu Feb 20 14:17:28 2014 +0100 +++ b/src/Pure/PIDE/markup_tree.scala Thu Feb 20 14:36:17 2014 +0100 @@ -176,7 +176,7 @@ if (body.forall(e => new_range.contains(e._1))) new Markup_Tree(branches -- body.keys, Entry(new_markup, new Markup_Tree(body))) else { - java.lang.System.err.println("Ignored overlapping markup information: " + new_markup + + System.err.println("Ignored overlapping markup information: " + new_markup + body.filter(e => !new_range.contains(e._1)).mkString("\n")) this }