src/Pure/PIDE/markup_tree.scala

--- a/src/Pure/PIDE/markup_tree.scala	Wed Jan 15 19:49:13 2020 +0100
+++ b/src/Pure/PIDE/markup_tree.scala	Wed Jan 15 19:54:50 2020 +0100
@@ -153,7 +153,7 @@
             new Markup_Tree(branches -- body.keys, Entry(new_markup, new Markup_Tree(body)))
           else {
             Output.warning("Ignored overlapping markup information: " + new_markup + "\n" +
-              body.filter(e => !new_range.contains(e._1)).map(_._2).mkString("\n"))
+              body.filter(e => !new_range.contains(e._1)).values.mkString("\n"))
             this
           }
         }