src/Pure/PIDE/markup_tree.scala
changeset 48762 9ff86bf6ad19
parent 47539 436ae5ea4f80
child 49417 c5a8592fb5d3
     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          }