# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1711465314 -3600
# Node ID 11a1f4d7af5151d66bd27e3eda809150abf2eb48
# Parent  dca9c237d108edc6bce09ff869192025012969b3
allow raw input in HTML (e.g., for web applications);

diff -r dca9c237d108 -r 11a1f4d7af51 src/Pure/General/html.scala
--- a/src/Pure/General/html.scala	Tue Mar 26 09:31:34 2024 +0100
+++ b/src/Pure/General/html.scala	Tue Mar 26 16:01:54 2024 +0100
@@ -239,6 +239,8 @@
       body foreach {
         case XML.Elem(markup, Nil) =>
           XML.output_elem(s, markup, end = true)
+        case XML.Elem(Markup(RAW, _), List(XML.Text(raw))) =>
+          s ++= raw
         case XML.Elem(markup, ts) =>
           if (structural && structural_elements(markup.name)) s += '\n'
           XML.output_elem(s, markup)
@@ -261,7 +263,10 @@
 
   /* 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 parse_document(html: String): Jsoup_Document = Jsoup.parse(html)
   def get_document(url: String): Jsoup_Document = Jsoup.connect(url).get()