author | wenzelm |
Fri, 10 Aug 2012 21:22:40 +0200 | |
changeset 48762 | 9ff86bf6ad19 |
parent 48761 | 6a355b4b6a59 |
child 48763 | de68fc11c245 |
--- 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 } }