# HG changeset patch
# User wenzelm
# Date 1733654995 -3600
# Node ID a25a456f81b74fbe6218d03853605d4a54416263
# Parent  8c005a92c65f8fc5c4c9fd7ea3a80f03b33fbae6
clarified signature;

diff -r 8c005a92c65f -r a25a456f81b7 src/Pure/Build/browser_info.scala
--- a/src/Pure/Build/browser_info.scala	Sun Dec 08 00:05:35 2024 +0100
+++ b/src/Pure/Build/browser_info.scala	Sun Dec 08 11:49:55 2024 +0100
@@ -521,7 +521,7 @@
                 case _ =>
                   body1
               }
-            Rendering.get_foreground(markup.name) orElse Rendering.get_text_color(markup) match {
+            Rendering.get_foreground_text_color(markup) match {
               case Some(c) => (html_class(c.toString, html), offset)
               case None => (html_class(markup.name, html), offset)
             }
diff -r 8c005a92c65f -r a25a456f81b7 src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Sun Dec 08 00:05:35 2024 +0100
+++ b/src/Pure/PIDE/rendering.scala	Sun Dec 08 11:49:55 2024 +0100
@@ -109,7 +109,8 @@
     if (Markup.has_syntax(markup.properties)) text_color2.get(markup.name)
     else text_color1.get(markup.name) orElse text_color2.get(markup.name)
 
-  def get_foreground(name: String): Option[Color.Value] = foreground.get(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,