src/Pure/PIDE/xml.scala

--- a/src/Pure/PIDE/xml.scala	Sun Oct 23 12:35:48 2016 +0200
+++ b/src/Pure/PIDE/xml.scala	Sun Oct 23 13:16:23 2016 +0200
@@ -26,6 +26,9 @@
   case class Elem(markup: Markup, body: Body) extends Tree
   {
     def name: String = markup.name
+    def update_attributes(more_attributes: Attributes): Elem =
+      if (more_attributes.isEmpty) this
+      else Elem(markup.update_properties(more_attributes), body)
   }
   case class Text(content: String) extends Tree