# HG changeset patch
# User wenzelm
# Date 1488906779 -3600
# Node ID 576d52aa0a78b7d9c468b19cb48cdb8b58de7d70
# Parent  b5782e99665162d59dd3693531fb560490795fa0
tuned;

diff -r b5782e996651 -r 576d52aa0a78 src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Tue Mar 07 17:56:57 2017 +0100
+++ b/src/Pure/PIDE/rendering.scala	Tue Mar 07 18:12:59 2017 +0100
@@ -52,7 +52,7 @@
       values -- background_colors -- foreground_colors -- message_underline_colors
 
     // text
-    val text = Value("text")
+    val main = Value("main")
     val keyword1 = Value("keyword1")
     val keyword2 = Value("keyword2")
     val keyword3 = Value("keyword3")
@@ -130,12 +130,12 @@
     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.STRING -> Color.main,
+    Markup.ALT_STRING -> Color.main,
+    Markup.VERBATIM -> Color.main,
+    Markup.CARTOUCHE -> Color.main,
     Markup.LITERAL -> Color.keyword1,
-    Markup.DELIMITER -> Color.text,
+    Markup.DELIMITER -> Color.main,
     Markup.TFREE -> Color.tfree,
     Markup.TVAR -> Color.tvar,
     Markup.FREE -> Color.free,
@@ -151,7 +151,7 @@
     Markup.ML_KEYWORD1 -> Color.keyword1,
     Markup.ML_KEYWORD2 -> Color.keyword2,
     Markup.ML_KEYWORD3 -> Color.keyword3,
-    Markup.ML_DELIMITER -> Color.text,
+    Markup.ML_DELIMITER -> Color.main,
     Markup.ML_NUMERAL -> Color.inner_numeral,
     Markup.ML_CHAR -> Color.inner_quoted,
     Markup.ML_STRING -> Color.inner_quoted,
diff -r b5782e996651 -r 576d52aa0a78 src/Tools/jEdit/src/jedit_rendering.scala
--- a/src/Tools/jEdit/src/jedit_rendering.scala	Tue Mar 07 17:56:57 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Tue Mar 07 18:12:59 2017 +0100
@@ -163,7 +163,7 @@
   /* colors */
 
   def color(s: String): Color =
-    if (s == "text_color") text_color
+    if (s == "main_color") main_color
     else Color_Value(options.string(s))
 
   def color(c: Rendering.Color.Value): Color = _rendering_colors(c)
@@ -171,7 +171,8 @@
   lazy val _rendering_colors: Map[Rendering.Color.Value, Color] =
     Rendering.Color.values.iterator.map(c => c -> color(c.toString + "_color")).toMap
 
-  val text_color = jEdit.getColorProperty("view.fgColor")
+  val main_color = jEdit.getColorProperty("view.fgColor")
+
   val outdated_color = color("outdated_color")
   val unprocessed_color = color("unprocessed_color")
   val running_color = color("running_color")