| changeset 73028 | 95e0f014cd24 |
| parent 73024 | 337e1b135d2f |
| child 73030 | 72a8fdfa185d |
--- a/src/Pure/PIDE/xml.scala Sat Jan 02 16:12:52 2021 +0100 +++ b/src/Pure/PIDE/xml.scala Sat Jan 02 16:30:43 2021 +0100 @@ -34,6 +34,7 @@ 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) + val no_text: Text = Text("") val newline: Text = Text("\n")