# HG changeset patch
# User wenzelm
# Date 1308402436 -7200
# Node ID 13afd4634ac3ddc8c8adb1bb451d4a398ae771f5
# Parent  ae6b0c3e58a83e54241f9a854f877f2dc1cdd852
tuned markup;

diff -r ae6b0c3e58a8 -r 13afd4634ac3 src/Tools/jEdit/src/isabelle_markup.scala
--- a/src/Tools/jEdit/src/isabelle_markup.scala	Sat Jun 18 14:48:56 2011 +0200
+++ b/src/Tools/jEdit/src/isabelle_markup.scala	Sat Jun 18 15:07:16 2011 +0200
@@ -112,6 +112,9 @@
 
   private val text_colors: Map[String, Color] =
     Map(
+      Markup.LITERAL -> keyword1_color,
+      Markup.DELIMITER -> get_color("black"),
+      Markup.IDENT -> get_color("black"),
       Markup.TCLASS -> get_color("red"),
       Markup.TFREE -> get_color("#A020F0"),
       Markup.TVAR -> get_color("#A020F0"),
@@ -123,8 +126,6 @@
       Markup.INNER_STRING -> get_color("#D2691E"),
       Markup.INNER_COMMENT -> get_color("#8B0000"),
       Markup.DYNAMIC_FACT -> get_color("yellowgreen"),
-      Markup.LITERAL -> keyword1_color,
-      Markup.DELIMITER -> get_color("black"),
       Markup.ML_KEYWORD -> keyword1_color,
       Markup.ML_DELIMITER -> get_color("black"),
       Markup.ML_NUMERAL -> get_color("red"),