# HG changeset patch
# User wenzelm
# Date 1442246623 -7200
# Node ID 1d9c121cbe4de5c87b8d12598fb8c1349c744ceb
# Parent  74eddfef841e6c906ae41decd467a341e156543c
avoid hardwired colors;

diff -r 74eddfef841e -r 1d9c121cbe4d src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Mon Sep 14 17:39:29 2015 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Mon Sep 14 18:03:43 2015 +0200
@@ -14,7 +14,7 @@
 import javax.swing.Icon
 
 import org.gjt.sp.jedit.syntax.{Token => JEditToken}
-import org.gjt.sp.jedit.{jEdit, View}
+import org.gjt.sp.jedit.jEdit
 
 import scala.collection.immutable.SortedMap
 
@@ -719,6 +719,8 @@
 
   /* 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,
@@ -726,12 +728,12 @@
       Markup.QUASI_KEYWORD -> quasi_keyword_color,
       Markup.IMPROPER -> improper_color,
       Markup.OPERATOR -> operator_color,
-      Markup.STRING -> Color.BLACK,
-      Markup.ALT_STRING -> Color.BLACK,
-      Markup.VERBATIM -> Color.BLACK,
-      Markup.CARTOUCHE -> Color.BLACK,
+      Markup.STRING -> foreground_color,
+      Markup.ALT_STRING -> foreground_color,
+      Markup.VERBATIM -> foreground_color,
+      Markup.CARTOUCHE -> foreground_color,
       Markup.LITERAL -> keyword1_color,
-      Markup.DELIMITER -> Color.BLACK,
+      Markup.DELIMITER -> foreground_color,
       Markup.TFREE -> tfree_color,
       Markup.TVAR -> tvar_color,
       Markup.FREE -> free_color,
@@ -746,7 +748,7 @@
       Markup.ML_KEYWORD1 -> keyword1_color,
       Markup.ML_KEYWORD2 -> keyword2_color,
       Markup.ML_KEYWORD3 -> keyword3_color,
-      Markup.ML_DELIMITER -> Color.BLACK,
+      Markup.ML_DELIMITER -> foreground_color,
       Markup.ML_NUMERAL -> inner_numeral_color,
       Markup.ML_CHAR -> inner_quoted_color,
       Markup.ML_STRING -> inner_quoted_color,