more operations (see also properties.ML);

--- a/src/Pure/General/properties.scala	Sun Oct 23 12:35:48 2016 +0200
+++ b/src/Pure/General/properties.scala	Sun Oct 23 13:16:23 2016 +0200
@@ -10,11 +10,30 @@
 
 object Properties
 {
-  /* named entries */
-
   type Entry = (java.lang.String, java.lang.String)
   type T = List[Entry]
 
+  def defined(props: T, name: java.lang.String): java.lang.Boolean =
+    props.exists({ case (x, _) => x == name })
+
+  def get(props: T, name: java.lang.String): Option[java.lang.String] =
+    props.collectFirst({ case (x, y) if x == name => y })
+
+  def put(props: T, entry: Entry): T =
+  {
+    val (x, y) = entry
+    def update(ps: T): T =
+      ps match {
+        case (p @ (x1, _)) :: rest =>
+          if (x1 == x) (x1, y) :: rest else p :: update(rest)
+        case Nil => Nil
+      }
+    if (defined(props, x)) update(props) else entry :: props
+  }
+
+
+  /* named entries */
+
   class String(val name: java.lang.String)
   {
     def apply(value: java.lang.String): T = List((name, value))

--- a/src/Pure/PIDE/markup.scala	Sun Oct 23 12:35:48 2016 +0200
+++ b/src/Pure/PIDE/markup.scala	Sun Oct 23 13:16:23 2016 +0200
@@ -602,4 +602,8 @@
 {
   def markup(s: String): String =
     YXML.string_of_tree(XML.Elem(this, List(XML.Text(s))))
+
+  def update_properties(more_props: Properties.T): Markup =
+    if (more_props.isEmpty) this
+    else Markup(name, (more_props :\ properties) { case (p, ps) => Properties.put(ps, p) })
 }

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