src/Pure/PIDE/markup.scala

--- a/src/Pure/PIDE/markup.scala	Sun May 07 13:42:20 2017 +0200
+++ b/src/Pure/PIDE/markup.scala	Sun May 07 16:04:19 2017 +0200
@@ -634,4 +634,7 @@
   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) })
+
+  def + (entry: Properties.Entry): Markup =
+    Markup(name, Properties.put(properties, entry))
 }