more robust: untyped/unscoped markup elements need to reside in module Markup for minimal static checking (see also 11a1f4d7af51);

--- 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()

--- a/src/Pure/PIDE/markup.scala	Tue Mar 26 21:25:35 2024 +0100
+++ b/src/Pure/PIDE/markup.scala	Tue Mar 26 21:34:08 2024 +0100
@@ -363,6 +363,11 @@
   }
 
 
+  /* HTML */
+
+  val RAW_HTML = "raw_html"
+
+
   /* LaTeX */
 
   val Document_Latex = new Markup_Elem("document_latex")