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