# HG changeset patch
# User wenzelm
# Date 1344626560 -7200
# Node ID 9ff86bf6ad19582407f64eaccdd3908e18f0cb19
# Parent  6a355b4b6a5972af5479efaf2309cee4db29136e
tuned message;

diff -r 6a355b4b6a59 -r 9ff86bf6ad19 src/Pure/PIDE/markup_tree.scala
--- a/src/Pure/PIDE/markup_tree.scala	Fri Aug 10 20:53:16 2012 +0200
+++ b/src/Pure/PIDE/markup_tree.scala	Fri Aug 10 21:22:40 2012 +0200
@@ -95,7 +95,8 @@
             new Markup_Tree(rest, Entry(new_markup, new Markup_Tree(body)))
           }
           else { // FIXME split markup!?
-            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
           }
         }