# HG changeset patch
# User wenzelm
# Date 1733604179 -3600
# Node ID 4eba973e8a7be2004f318b4c548484e95a357b61
# Parent  a7879978d15dacb3cda9852d3e872d18c2495d8a
clarified signature: more explicit operations;

diff -r a7879978d15d -r 4eba973e8a7b src/Pure/Build/browser_info.scala
--- a/src/Pure/Build/browser_info.scala	Sat Dec 07 16:07:48 2024 +0100
+++ b/src/Pure/Build/browser_info.scala	Sat Dec 07 21:42:59 2024 +0100
@@ -522,7 +522,7 @@
                 case _ =>
                   body1
               }
-            Rendering.foreground.get(name) orElse Rendering.text_color.get(name) match {
+            Rendering.foreground.get(name) orElse Rendering.get_text_color(name) match {
               case Some(c) => (html_class(c.toString, html), offset)
               case None => (html_class(name, html), offset)
             }
diff -r a7879978d15d -r 4eba973e8a7b src/Pure/PIDE/rendering.scala
--- 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,
diff -r a7879978d15d -r 4eba973e8a7b src/Tools/VSCode/src/pretty_text_panel.scala
--- a/src/Tools/VSCode/src/pretty_text_panel.scala	Sat Dec 07 16:07:48 2024 +0100
+++ b/src/Tools/VSCode/src/pretty_text_panel.scala	Sat Dec 07 21:42:59 2024 +0100
@@ -79,7 +79,8 @@
           { case (_, m) => Some(Some(m.info.name)) }
         ).flatMap(e => e.info match {
           case None => None
-          case Some(i) => Some((document.range(e._1), "text_" ++ Rendering.text_color(i).toString))
+          case Some(name) =>
+            Some((document.range(e._1), "text_" ++ Rendering.get_text_color(name).get.toString))
         })
         .groupMap(_._2)(e => LSP.Decoration_Options(e._1, List())).toList
 
diff -r a7879978d15d -r 4eba973e8a7b src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Sat Dec 07 16:07:48 2024 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Sat Dec 07 21:42:59 2024 +0100
@@ -167,7 +167,7 @@
   def text_color(range: Text.Range): List[Text.Info[Rendering.Color.Value]] = {
     snapshot.select(range, Rendering.text_color_elements, _ =>
       {
-        case Text.Info(_, elem) => Rendering.text_color.get(elem.name)
+        case Text.Info(_, elem) => Rendering.get_text_color(elem.name)
       })
   }
 
diff -r a7879978d15d -r 4eba973e8a7b src/Tools/jEdit/src/jedit_rendering.scala
--- a/src/Tools/jEdit/src/jedit_rendering.scala	Sat Dec 07 16:07:48 2024 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Sat Dec 07 21:42:59 2024 +0100
@@ -375,7 +375,7 @@
     else
       snapshot.cumulate(range, current_color, Rendering.text_color_elements, _ =>
         {
-          case (_, Text.Info(_, elem)) => Rendering.text_color.get(elem.name).map(color)
+          case (_, Text.Info(_, elem)) => Rendering.get_text_color(elem.name).map(color)
         })
   }