diff -r ed7b5cd3a7f2 -r 787e5ee6ef53 src/Pure/PIDE/xml.scala
--- a/src/Pure/PIDE/xml.scala	Sun May 07 13:42:20 2017 +0200
+++ b/src/Pure/PIDE/xml.scala	Sun May 07 16:04:19 2017 +0200
@@ -18,6 +18,7 @@
 
   /* datatype representation */
 
+  type Attribute = Properties.Entry
   type Attributes = Properties.T
 
   sealed abstract class Tree { override def toString: String = string_of_tree(this) }
@@ -25,9 +26,12 @@
   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)
+
+    def + (att: Attribute): Tree = Elem(markup + att, body)
   }
   case class Text(content: String) extends Tree