# HG changeset patch # User wenzelm # Date 1733664426 -3600 # Node ID d387683ea725845773c9f3ec7ba7e186a908bc28 # Parent a25a456f81b74fbe6218d03853605d4a54416263 more accurate HTML markup: suppress text_color that has_syntax (amending b57996a0688c); diff -r a25a456f81b7 -r d387683ea725 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))