diff -r bf19ea589f99 -r f207acb03ccb src/Pure/Build/browser_info.scala --- a/src/Pure/Build/browser_info.scala Sun Dec 08 20:09:14 2024 +0100 +++ b/src/Pure/Build/browser_info.scala Sun Dec 08 20:13:40 2024 +0100 @@ -158,6 +158,7 @@ val default_elements: Elements = Elements( html = Rendering.foreground_elements ++ Rendering.text_color_elements + + Markup.TCLASS + Markup.TCONST + Markup.CONST + Markup.NUMERAL + Markup.COMMENT + Markup.ENTITY + Markup.LANGUAGE + Markup.PATH + Markup.URL, entity = Markup.Elements(Markup.THEORY, Markup.TYPE_NAME, Markup.CONSTANT, Markup.FACT,