--- a/src/Pure/PIDE/markup_tree.scala Fri Sep 26 09:58:35 2014 +0200
+++ b/src/Pure/PIDE/markup_tree.scala Fri Sep 26 14:29:06 2014 +0200
@@ -153,8 +153,8 @@
if (body.forall(e => new_range.contains(e._1)))
new Markup_Tree(branches -- body.keys, Entry(new_markup, new Markup_Tree(body)))
else {
- Output.warning("Ignored overlapping markup information: " + new_markup +
- body.filter(e => !new_range.contains(e._1)).mkString("\n"))
+ Output.warning("Ignored overlapping markup information: " + new_markup + "\n" +
+ body.filter(e => !new_range.contains(e._1)).map(_._2).mkString("\n"))
this
}
}