| changeset 66196 | 31c9b09cc1d4 |
| parent 65991 | fa787e233214 |
| child 67109 | 5fce3a24e476 |
--- a/src/Pure/PIDE/xml.scala Mon Jun 26 15:57:20 2017 +0200 +++ b/src/Pure/PIDE/xml.scala Mon Jun 26 23:12:39 2017 +0200 @@ -35,6 +35,7 @@ } case class Text(content: String) extends Tree + def elem(markup: Markup): XML.Elem = XML.Elem(markup, Nil) def elem(name: String, body: Body): XML.Elem = XML.Elem(Markup(name, Nil), body) def elem(name: String): XML.Elem = XML.Elem(Markup(name, Nil), Nil)