more accurate HTML markup: suppress text_color that has_syntax (amending b57996a0688c);
authorwenzelm
Sun, 08 Dec 2024 14:27:06 +0100
changeset 81562 d387683ea725
parent 81561 a25a456f81b7
child 81563 c4c983c5c7f2
more accurate HTML markup: suppress text_color that has_syntax (amending b57996a0688c);
src/Pure/Build/browser_info.scala
--- a/src/Pure/Build/browser_info.scala	Sun Dec 08 11:49:55 2024 +0100
+++ b/src/Pure/Build/browser_info.scala	Sun Dec 08 14:27:06 2024 +0100
@@ -478,7 +478,8 @@
       @tailrec
       def html_body_single(xml_tree: XML.Tree, end_offset: Symbol.Offset): (XML.Body, Symbol.Offset) =
         xml_tree match {
-          case XML.Wrapped_Elem(markup, _, body) => html_body_single(XML.Elem(markup, body), end_offset)
+          case XML.Wrapped_Elem(markup, _, body) =>
+            html_body_single(XML.Elem(markup, body), end_offset)
           case XML.Elem(Markup(Markup.ENTITY, props @ Markup.Kind(kind)), body) =>
             val (body1, offset) = html_body(body, end_offset)
             if (elements.entity(kind)) {
@@ -521,10 +522,14 @@
                 case _ =>
                   body1
               }
-            Rendering.get_foreground_text_color(markup) match {
-              case Some(c) => (html_class(c.toString, html), offset)
-              case None => (html_class(markup.name, html), offset)
-            }
+            val c =
+              Rendering.get_foreground_text_color(markup) match {
+                case Some(color) => color.toString
+                case None =>
+                  if (Rendering.get_foreground_text_color(Markup(markup.name, Nil)).nonEmpty) ""
+                  else markup.name
+              }
+            (html_class(c, html), offset)
           case XML.Text(text) =>
             val offset = end_offset - Symbol.length(text)
             val body = HTML.text(Symbol.decode(text))