# HG changeset patch
# User wenzelm
# Date 1308058337 -7200
# Node ID 34492601c0e003f006eb8adce8cf993be2718693
# Parent  a59ae768249e1e85c1a6133d9b7fb5c977aadc43
tuned colors;

diff -r a59ae768249e -r 34492601c0e0 src/Tools/jEdit/src/isabelle_markup.scala
--- a/src/Tools/jEdit/src/isabelle_markup.scala	Tue Jun 14 14:55:22 2011 +0200
+++ b/src/Tools/jEdit/src/isabelle_markup.scala	Tue Jun 14 15:32:17 2011 +0200
@@ -33,6 +33,9 @@
   val bad_color = new Color(255, 106, 106, 100)
   val hilite_color = new Color(255, 204, 102, 100)
 
+  val keyword1_color = get_color("#006699")
+  val keyword2_color = get_color("#009966")
+
   class Icon(val priority: Int, val icon: javax.swing.Icon)
   {
     def >= (that: Icon): Boolean = this.priority >= that.priority
@@ -118,8 +121,8 @@
       Markup.INNER_STRING -> get_color("#D2691E"),
       Markup.INNER_COMMENT -> get_color("#8B0000"),
       Markup.DYNAMIC_FACT -> get_color("yellowgreen"),
-      Markup.LITERAL -> get_color("black"),
-      Markup.ML_KEYWORD -> get_color("grey"),
+      Markup.LITERAL -> keyword1_color,
+      Markup.ML_KEYWORD -> keyword1_color,
       Markup.ML_DELIMITER -> get_color("black"),
       Markup.ML_NUMERAL -> get_color("red"),
       Markup.ML_CHAR -> get_color("#D2691E"),