# HG changeset patch
# User wenzelm
# Date 1733681105 -3600
# Node ID 56075edacb1082255fd7b029fde13b190ea02093
# Parent  c4c983c5c7f211325d7bb1495bb62c4740b2b090
tuned: more robust wrt. changes the Markup space;

diff -r c4c983c5c7f2 -r 56075edacb10 src/Pure/Build/browser_info.scala
--- a/src/Pure/Build/browser_info.scala	Sun Dec 08 15:12:20 2024 +0100
+++ b/src/Pure/Build/browser_info.scala	Sun Dec 08 19:05:05 2024 +0100
@@ -523,11 +523,12 @@
                   body1
               }
             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
+              if (Markup.has_syntax(markup.properties)) ""
+              else {
+                Rendering.get_foreground_text_color(markup) match {
+                  case Some(color) => color.toString
+                  case None => markup.name
+                }
               }
             (html_class(c, html), offset)
           case XML.Text(text) =>
diff -r c4c983c5c7f2 -r 56075edacb10 src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Sun Dec 08 15:12:20 2024 +0100
+++ b/src/Pure/PIDE/rendering.scala	Sun Dec 08 19:05:05 2024 +0100
@@ -106,22 +106,18 @@
   /* text color */
 
   def get_text_color(markup: Markup): Option[Color.Value] =
-    if (Markup.has_syntax(markup.properties)) text_color2.get(markup.name)
-    else text_color1.get(markup.name) orElse text_color2.get(markup.name)
+    if (Markup.has_syntax(markup.properties)) None
+    else text_color.get(markup.name)
 
   def get_foreground_text_color(markup: Markup): Option[Color.Value] =
     foreground.get(markup.name) orElse get_text_color(markup)
 
-  private val text_color1 = Map(
-    Markup.IMPROPER -> Color.improper,
-    Markup.FREE -> Color.free,
-    Markup.SKOLEM -> Color.skolem)
-
-  private val text_color2 = Map(
+  val text_color = Map(
     Markup.KEYWORD1 -> Color.keyword1,
     Markup.KEYWORD2 -> Color.keyword2,
     Markup.KEYWORD3 -> Color.keyword3,
     Markup.QUASI_KEYWORD -> Color.quasi_keyword,
+    Markup.IMPROPER -> Color.improper,
     Markup.OPERATOR -> Color.operator,
     Markup.STRING -> Color.main,
     Markup.ALT_STRING -> Color.main,
@@ -130,6 +126,8 @@
     Markup.DELIMITER -> Color.main,
     Markup.TFREE -> Color.tfree,
     Markup.TVAR -> Color.tvar,
+    Markup.FREE -> Color.free,
+    Markup.SKOLEM -> Color.skolem,
     Markup.BOUND -> Color.bound,
     Markup.VAR -> Color.`var`,
     Markup.INNER_STRING -> Color.inner_quoted,
@@ -232,7 +230,7 @@
   val foreground_elements: Markup.Elements = Markup.Elements(foreground.keySet)
 
   val text_color_elements: Markup.Elements =
-    Markup.Elements(text_color1.keySet ++ text_color2.keySet)
+    Markup.Elements(text_color.keySet)
 
   val structure_elements: Markup.Elements =
     Markup.Elements(Markup.NOTATION, Markup.EXPRESSION, Markup.LANGUAGE, Markup.ML_TYPING,