--- 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,
--- 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")