--- 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