src/Pure/PIDE/markup.scala
changeset 65753 787e5ee6ef53
parent 65335 7634d33c1a79
child 65937 fde7b5d209d5
     1.1 --- a/src/Pure/PIDE/markup.scala	Sun May 07 13:42:20 2017 +0200
     1.2 +++ b/src/Pure/PIDE/markup.scala	Sun May 07 16:04:19 2017 +0200
     1.3 @@ -634,4 +634,7 @@
     1.4    def update_properties(more_props: Properties.T): Markup =
     1.5      if (more_props.isEmpty) this
     1.6      else Markup(name, (more_props :\ properties) { case (p, ps) => Properties.put(ps, p) })
     1.7 +
     1.8 +  def + (entry: Properties.Entry): Markup =
     1.9 +    Markup(name, Properties.put(properties, entry))
    1.10  }