src/Pure/PIDE/markup.scala
changeset 64358 15c90b744481
parent 63681 d2448471ffba
child 64370 865b39487b5d
     1.1 --- a/src/Pure/PIDE/markup.scala	Sun Oct 23 12:35:48 2016 +0200
     1.2 +++ b/src/Pure/PIDE/markup.scala	Sun Oct 23 13:16:23 2016 +0200
     1.3 @@ -602,4 +602,8 @@
     1.4  {
     1.5    def markup(s: String): String =
     1.6      YXML.string_of_tree(XML.Elem(this, List(XML.Text(s))))
     1.7 +
     1.8 +  def update_properties(more_props: Properties.T): Markup =
     1.9 +    if (more_props.isEmpty) this
    1.10 +    else Markup(name, (more_props :\ properties) { case (p, ps) => Properties.put(ps, p) })
    1.11  }