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