# HG changeset patch
# User wenzelm
# Date 1314453684 -7200
# Node ID 794a32d58c77e0a7d1e51cb3353ff5b55f781d84
# Parent  3c40007aa0316c478502500b02de372bba2a31bd
tuned colors;

diff -r 3c40007aa031 -r 794a32d58c77 src/Tools/jEdit/src/isabelle_markup.scala
--- a/src/Tools/jEdit/src/isabelle_markup.scala	Sat Aug 27 15:53:18 2011 +0200
+++ b/src/Tools/jEdit/src/isabelle_markup.scala	Sat Aug 27 16:01:24 2011 +0200
@@ -33,10 +33,7 @@
   val bad_color = new Color(255, 106, 106, 100)
   val hilite_color = new Color(255, 204, 102, 100)
 
-  val string_color = new Color(0, 139, 0, 20)
-  val altstring_color = new Color(139, 139, 0, 20)
-  val verbatim_color = new Color(0, 0, 139, 20)
-
+  val quoted_color = new Color(139, 139, 139, 25)
   val subexp_color = new Color(80, 80, 80, 50)
 
   val keyword1_color = get_color("#006699")
@@ -116,9 +113,9 @@
 
   val foreground: Markup_Tree.Select[Color] =
   {
-    case Text.Info(_, XML.Elem(Markup(Markup.STRING, _), _)) => string_color
-    case Text.Info(_, XML.Elem(Markup(Markup.ALTSTRING, _), _)) => altstring_color
-    case Text.Info(_, XML.Elem(Markup(Markup.VERBATIM, _), _)) => verbatim_color
+    case Text.Info(_, XML.Elem(Markup(Markup.STRING, _), _)) => quoted_color
+    case Text.Info(_, XML.Elem(Markup(Markup.ALTSTRING, _), _)) => quoted_color
+    case Text.Info(_, XML.Elem(Markup(Markup.VERBATIM, _), _)) => quoted_color
   }
 
   private val text_entity_colors: Map[String, Color] =