--- 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")
--- a/src/Pure/PIDE/yxml.scala Sat Jan 02 16:12:52 2021 +0100
+++ b/src/Pure/PIDE/yxml.scala Sat Jan 02 16:30:43 2021 +0100
@@ -125,7 +125,7 @@
def parse(source: CharSequence): XML.Tree =
parse_body(source) match {
case List(result) => result
- case Nil => XML.Text("")
+ case Nil => XML.no_text
case _ => err("multiple XML trees")
}
--- a/src/Pure/Thy/html.scala Sat Jan 02 16:12:52 2021 +0100
+++ b/src/Pure/Thy/html.scala Sat Jan 02 16:30:43 2021 +0100
@@ -153,7 +153,6 @@
/* structured markup operators */
def text(txt: String): XML.Body = if (txt.isEmpty) Nil else List(XML.Text(txt))
- val no_text: XML.Tree = XML.Text("")
val break: XML.Body = List(XML.elem("br"))
val nl: XML.Body = List(XML.Text("\n"))
--- a/src/Pure/Thy/presentation.scala Sat Jan 02 16:12:52 2021 +0100
+++ b/src/Pure/Thy/presentation.scala Sat Jan 02 16:30:43 2021 +0100
@@ -67,7 +67,7 @@
}
private def html_class(c: String, html: XML.Body): XML.Tree =
- if (html.forall(_ == HTML.no_text)) HTML.no_text
+ if (html.forall(_ == XML.no_text)) XML.no_text
else if (html_div(html)) HTML.div(c, html)
else HTML.span(c, html)
@@ -77,7 +77,7 @@
html_class(Markup.Language.DOCUMENT, html_body(body))
case XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), body) => HTML.par(html_body(body))
case XML.Elem(Markup(Markup.MARKDOWN_ITEM, _), body) => HTML.item(html_body(body))
- case XML.Elem(Markup(Markup.Markdown_Bullet.name, _), _) => HTML.no_text
+ case XML.Elem(Markup(Markup.Markdown_Bullet.name, _), _) => XML.no_text
case XML.Elem(Markup.Markdown_List(kind), body) =>
if (kind == Markup.ENUMERATE) HTML.enum(html_body(body)) else HTML.list(html_body(body))
case XML.Elem(markup, body) =>