# HG changeset patch
# User wenzelm
# Date 1348750206 -7200
# Node ID ce1c34c98eebcc590b806b408466a1ef82257a66
# Parent  b610c0d52bfa25cfdbe9978a5b5432584a5263a7
tuned;

diff -r b610c0d52bfa -r ce1c34c98eeb src/Pure/PIDE/markup_tree.scala
--- a/src/Pure/PIDE/markup_tree.scala	Thu Sep 27 14:46:34 2012 +0200
+++ b/src/Pure/PIDE/markup_tree.scala	Thu Sep 27 14:50:06 2012 +0200
@@ -133,8 +133,8 @@
           val body = overlapping(new_range)
           if (body.forall(e => new_range.contains(e._1)))
             new Markup_Tree(branches -- body.keys, Entry(new_markup, new Markup_Tree(body)))
-          else { // FIXME split markup!?
-            System.err.println("Ignored overlapping markup information: " + new_markup +
+          else {
+            java.lang.System.err.println("Ignored overlapping markup information: " + new_markup +
               body.filter(e => !new_range.contains(e._1)).mkString("\n"))
             this
           }