# HG changeset patch
# User wenzelm
# Date 1711485858 -3600
# Node ID ac4412562c7b1d27cfc6b2c131c6fedaa76f216f
# Parent  fb96063456fd6ffde3cbb1cb2e7bd01612d90e21
more robust XML body: allow empty text, as well as arbitrary pro-forma markup (e.g. see XML.blob in Isabelle/ML);

diff -r fb96063456fd -r ac4412562c7b src/Pure/General/html.scala
--- a/src/Pure/General/html.scala	Tue Mar 26 21:34:08 2024 +0100
+++ b/src/Pure/General/html.scala	Tue Mar 26 21:44:18 2024 +0100
@@ -239,8 +239,8 @@
       body foreach {
         case XML.Elem(markup, Nil) =>
           XML.output_elem(s, markup, end = true)
-        case XML.Elem(Markup(Markup.RAW_HTML, _), List(XML.Text(raw))) =>
-          s ++= raw
+        case XML.Elem(Markup(Markup.RAW_HTML, _), body) =>
+          XML.traverse_text(body)(()) { case (_, raw) => s.append(raw) }
         case XML.Elem(markup, ts) =>
           if (structural && structural_elements(markup.name)) s += '\n'
           XML.output_elem(s, markup)
@@ -263,8 +263,9 @@
 
   /* input */
 
+  def input_raw(text: String): XML.Elem = raw(HTML.text(input(text)))
   def input(text: String): String = Jsoup_Entities.unescape(text)
-  def input_raw(text: String): XML.Elem = XML.elem(Markup.RAW_HTML, List(XML.Text(input(text))))
+  def raw(body: XML.Body): XML.Elem = XML.elem(Markup.RAW_HTML, body)
 
   def parse_document(html: String): Jsoup_Document = Jsoup.parse(html)
   def get_document(url: String): Jsoup_Document = Jsoup.connect(url).get()