1.1 --- a/src/Pure/PIDE/markup_tree.scala Fri Aug 10 20:53:16 2012 +0200
1.2 +++ b/src/Pure/PIDE/markup_tree.scala Fri Aug 10 21:22:40 2012 +0200
1.3 @@ -95,7 +95,8 @@
1.4 new Markup_Tree(rest, Entry(new_markup, new Markup_Tree(body)))
1.5 }
1.6 else { // FIXME split markup!?
1.7 - 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 }
1.12 }