# HG changeset patch
# User wenzelm
# Date 1488905817 -3600
# Node ID b5782e99665162d59dd3693531fb560490795fa0
# Parent  36cd85caf09a219ff70f5e6100287843aa00eb97
more generic colors;

diff -r 36cd85caf09a -r b5782e996651 src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Tue Mar 07 17:21:41 2017 +0100
+++ b/src/Pure/PIDE/rendering.scala	Tue Mar 07 17:56:57 2017 +0100
@@ -50,6 +50,31 @@
     val error_message = Value("error_message")
     val message_background_colors =
       values -- background_colors -- foreground_colors -- message_underline_colors
+
+    // text
+    val text = Value("text")
+    val keyword1 = Value("keyword1")
+    val keyword2 = Value("keyword2")
+    val keyword3 = Value("keyword3")
+    val quasi_keyword = Value("quasi_keyword")
+    val improper = Value("improper")
+    val operator = Value("operator")
+    val tfree = Value("tfree")
+    val tvar = Value("tvar")
+    val free = Value("free")
+    val skolem = Value("skolem")
+    val bound = Value("bound")
+    val var_ = Value("var")
+    val inner_numeral = Value("inner_numeral")
+    val inner_quoted = Value("inner_quoted")
+    val inner_cartouche = Value("inner_cartouche")
+    val inner_comment = Value("inner_comment")
+    val dynamic = Value("dynamic")
+    val class_parameter = Value("class_parameter")
+    val antiquote = Value("antiquote")
+    val text_colors =
+      values -- background_colors -- foreground_colors -- message_underline_colors --
+      message_background_colors
   }
 
 
@@ -96,6 +121,45 @@
     error_pri -> Color.error_message)
 
 
+  /* text color */
+
+  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.text,
+    Markup.ALT_STRING -> Color.text,
+    Markup.VERBATIM -> Color.text,
+    Markup.CARTOUCHE -> Color.text,
+    Markup.LITERAL -> Color.keyword1,
+    Markup.DELIMITER -> Color.text,
+    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,
+    Markup.INNER_CARTOUCHE -> Color.inner_cartouche,
+    Markup.INNER_COMMENT -> Color.inner_comment,
+    Markup.DYNAMIC_FACT -> Color.dynamic,
+    Markup.CLASS_PARAMETER -> Color.class_parameter,
+    Markup.ANTIQUOTE -> Color.antiquote,
+    Markup.ML_KEYWORD1 -> Color.keyword1,
+    Markup.ML_KEYWORD2 -> Color.keyword2,
+    Markup.ML_KEYWORD3 -> Color.keyword3,
+    Markup.ML_DELIMITER -> Color.text,
+    Markup.ML_NUMERAL -> Color.inner_numeral,
+    Markup.ML_CHAR -> Color.inner_quoted,
+    Markup.ML_STRING -> Color.inner_quoted,
+    Markup.ML_COMMENT -> Color.inner_comment,
+    Markup.SML_STRING -> Color.inner_quoted,
+    Markup.SML_COMMENT -> Color.inner_comment)
+
+
   /* markup elements */
 
   val active_elements =
@@ -142,6 +206,8 @@
     Pretty.block(XML.Text(kind) :: Pretty.brk(1) :: body)
 
   val caret_focus_elements = Markup.Elements(Markup.ENTITY)
+
+  val text_color_elements = Markup.Elements(text_color.keySet)
 }
 
 abstract class Rendering(
diff -r 36cd85caf09a -r b5782e996651 src/Tools/jEdit/src/jedit_rendering.scala
--- a/src/Tools/jEdit/src/jedit_rendering.scala	Tue Mar 07 17:21:41 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Tue Mar 07 17:56:57 2017 +0100
@@ -162,13 +162,16 @@
 {
   /* colors */
 
-  def color(s: String): Color = Color_Value(options.string(s))
+  def color(s: String): Color =
+    if (s == "text_color") text_color
+    else Color_Value(options.string(s))
+
+  def color(c: Rendering.Color.Value): Color = _rendering_colors(c)
 
   lazy val _rendering_colors: Map[Rendering.Color.Value, Color] =
     Rendering.Color.values.iterator.map(c => c -> color(c.toString + "_color")).toMap
 
-  def color(c: Rendering.Color.Value): Color = _rendering_colors(c)
-
+  val text_color = jEdit.getColorProperty("view.fgColor")
   val outdated_color = color("outdated_color")
   val unprocessed_color = color("unprocessed_color")
   val running_color = color("running_color")
@@ -181,33 +184,13 @@
   val breakpoint_disabled_color = color("breakpoint_disabled_color")
   val breakpoint_enabled_color = color("breakpoint_enabled_color")
   val caret_debugger_color = color("caret_debugger_color")
-  val antiquote_color = color("antiquote_color")
   val highlight_color = color("highlight_color")
   val hyperlink_color = color("hyperlink_color")
   val active_hover_color = color("active_hover_color")
-  val keyword1_color = color("keyword1_color")
-  val keyword2_color = color("keyword2_color")
-  val keyword3_color = color("keyword3_color")
-  val quasi_keyword_color = color("quasi_keyword_color")
-  val improper_color = color("improper_color")
-  val operator_color = color("operator_color")
   val caret_invisible_color = color("caret_invisible_color")
   val completion_color = color("completion_color")
   val search_color = color("search_color")
 
-  val tfree_color = color("tfree_color")
-  val tvar_color = color("tvar_color")
-  val free_color = color("free_color")
-  val skolem_color = color("skolem_color")
-  val bound_color = color("bound_color")
-  val var_color = color("var_color")
-  val inner_numeral_color = color("inner_numeral_color")
-  val inner_quoted_color = color("inner_quoted_color")
-  val inner_cartouche_color = color("inner_cartouche_color")
-  val inner_comment_color = color("inner_comment_color")
-  val dynamic_color = color("dynamic_color")
-  val class_parameter_color = color("class_parameter_color")
-
 
   /* indentation */
 
@@ -463,54 +446,13 @@
 
   /* text color */
 
-  val foreground_color = jEdit.getColorProperty("view.fgColor")
-
-  private lazy val text_colors: Map[String, Color] = Map(
-      Markup.KEYWORD1 -> keyword1_color,
-      Markup.KEYWORD2 -> keyword2_color,
-      Markup.KEYWORD3 -> keyword3_color,
-      Markup.QUASI_KEYWORD -> quasi_keyword_color,
-      Markup.IMPROPER -> improper_color,
-      Markup.OPERATOR -> operator_color,
-      Markup.STRING -> foreground_color,
-      Markup.ALT_STRING -> foreground_color,
-      Markup.VERBATIM -> foreground_color,
-      Markup.CARTOUCHE -> foreground_color,
-      Markup.LITERAL -> keyword1_color,
-      Markup.DELIMITER -> foreground_color,
-      Markup.TFREE -> tfree_color,
-      Markup.TVAR -> tvar_color,
-      Markup.FREE -> free_color,
-      Markup.SKOLEM -> skolem_color,
-      Markup.BOUND -> bound_color,
-      Markup.VAR -> var_color,
-      Markup.INNER_STRING -> inner_quoted_color,
-      Markup.INNER_CARTOUCHE -> inner_cartouche_color,
-      Markup.INNER_COMMENT -> inner_comment_color,
-      Markup.DYNAMIC_FACT -> dynamic_color,
-      Markup.CLASS_PARAMETER -> class_parameter_color,
-      Markup.ANTIQUOTE -> antiquote_color,
-      Markup.ML_KEYWORD1 -> keyword1_color,
-      Markup.ML_KEYWORD2 -> keyword2_color,
-      Markup.ML_KEYWORD3 -> keyword3_color,
-      Markup.ML_DELIMITER -> foreground_color,
-      Markup.ML_NUMERAL -> inner_numeral_color,
-      Markup.ML_CHAR -> inner_quoted_color,
-      Markup.ML_STRING -> inner_quoted_color,
-      Markup.ML_COMMENT -> inner_comment_color,
-      Markup.SML_STRING -> inner_quoted_color,
-      Markup.SML_COMMENT -> inner_comment_color)
-
-  private lazy val text_color_elements =
-    Markup.Elements(text_colors.keySet)
-
-  def text_color(range: Text.Range, color: Color): List[Text.Info[Color]] =
+  def text_color(range: Text.Range, current_color: Color): List[Text.Info[Color]] =
   {
-    if (color == Token_Markup.hidden_color) List(Text.Info(range, color))
+    if (current_color == Token_Markup.hidden_color) List(Text.Info(range, current_color))
     else
-      snapshot.cumulate(range, color, text_color_elements, _ =>
+      snapshot.cumulate(range, current_color, Rendering.text_color_elements, _ =>
         {
-          case (_, Text.Info(_, elem)) => text_colors.get(elem.name)
+          case (_, Text.Info(_, elem)) => Rendering.text_color.get(elem.name).map(color(_))
         })
   }