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,