--- a/src/Pure/PIDE/rendering.scala Sat Dec 07 16:07:48 2024 +0100
+++ b/src/Pure/PIDE/rendering.scala Sat Dec 07 21:42:59 2024 +0100
@@ -105,7 +105,9 @@
/* text color */
- val text_color = Map(
+ def get_text_color(name: String): Option[Color.Value] = text_colors.get(name)
+
+ private val text_colors = Map(
Markup.KEYWORD1 -> Color.keyword1,
Markup.KEYWORD2 -> Color.keyword2,
Markup.KEYWORD3 -> Color.keyword3,
@@ -220,7 +222,7 @@
val foreground_elements = Markup.Elements(foreground.keySet)
- val text_color_elements = Markup.Elements(text_color.keySet)
+ val text_color_elements = Markup.Elements(text_colors.keySet)
val structure_elements =
Markup.Elements(Markup.NOTATION, Markup.EXPRESSION, Markup.LANGUAGE, Markup.ML_TYPING,