# HG changeset patch
# User wenzelm
# Date 1609601443 -3600
# Node ID 95e0f014cd24cd7a9d0d09d3093b81045d82b4d4
# Parent  000bcf2524fde0a1023ec900fb81296c4202ad7d
tuned signature;

diff -r 000bcf2524fd -r 95e0f014cd24 src/Pure/PIDE/xml.scala
--- 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")
 
 
diff -r 000bcf2524fd -r 95e0f014cd24 src/Pure/PIDE/yxml.scala
--- 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")
     }
 
diff -r 000bcf2524fd -r 95e0f014cd24 src/Pure/Thy/html.scala
--- 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"))
 
diff -r 000bcf2524fd -r 95e0f014cd24 src/Pure/Thy/presentation.scala
--- 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) =>