| changeset 59707 | 10effab11669 |
| parent 59369 | 7090199d3f78 |
| child 60744 | 4eba53a0ac3d |
--- a/src/Pure/PIDE/markup.scala Sun Mar 15 21:57:10 2015 +0100 +++ b/src/Pure/PIDE/markup.scala Sun Mar 15 22:05:08 2015 +0100 @@ -504,4 +504,7 @@ sealed case class Markup(name: String, properties: Properties.T) - +{ + def markup(s: String): String = + YXML.string_of_tree(XML.Elem(this, List(XML.Text(s)))) +}