# HG changeset patch
# User wenzelm
# Date 1411734546 -7200
# Node ID 0bf0e9788d54ad5eff4ef24d1e389e829ee3631a
# Parent  126c353540fc081be30ce08a10c14f9d8da332f6
tuned message;

diff -r 126c353540fc -r 0bf0e9788d54 src/Pure/PIDE/markup_tree.scala
--- 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
           }
         }