# HG changeset patch
# User wenzelm
# Date 1314453198 -7200
# Node ID 3c40007aa0316c478502500b02de372bba2a31bd
# Parent  da5f0af32c1b02583b4a4d8aca36aecdf72f0de5
transparent foreground color for quoted entities;

diff -r da5f0af32c1b -r 3c40007aa031 src/Tools/jEdit/src/isabelle_markup.scala
--- a/src/Tools/jEdit/src/isabelle_markup.scala	Sat Aug 27 13:26:06 2011 +0200
+++ b/src/Tools/jEdit/src/isabelle_markup.scala	Sat Aug 27 15:53:18 2011 +0200
@@ -33,7 +33,11 @@
   val bad_color = new Color(255, 106, 106, 100)
   val hilite_color = new Color(255, 204, 102, 100)
 
-  val subexp_color = new Color(0xC0, 0xC0, 0xC0, 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 subexp_color = new Color(80, 80, 80, 50)
 
   val keyword1_color = get_color("#006699")
   val keyword2_color = get_color("#009966")
@@ -110,6 +114,13 @@
     case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color
   }
 
+  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
+  }
+
   private val text_entity_colors: Map[String, Color] =
     Map(
       Markup.CLASS -> get_color("red"),
@@ -118,6 +129,9 @@
 
   private val text_colors: Map[String, Color] =
     Map(
+      Markup.STRING -> get_color("black"),
+      Markup.ALTSTRING -> get_color("black"),
+      Markup.VERBATIM -> get_color("black"),
       Markup.LITERAL -> keyword1_color,
       Markup.DELIMITER -> get_color("black"),
       Markup.IDENT -> get_color("black"),
diff -r da5f0af32c1b -r 3c40007aa031 src/Tools/jEdit/src/text_area_painter.scala
--- a/src/Tools/jEdit/src/text_area_painter.scala	Sat Aug 27 13:26:06 2011 +0200
+++ b/src/Tools/jEdit/src/text_area_painter.scala	Sat Aug 27 15:53:18 2011 +0200
@@ -313,6 +313,16 @@
           if (physical_lines(i) != -1) {
             val line_range = doc_view.proper_line_range(start(i), end(i))
 
+            // foreground color
+            for {
+              Text.Info(range, Some(color)) <-
+                snapshot.select_markup(line_range)(Isabelle_Markup.foreground).iterator
+              r <- Isabelle.gfx_range(text_area, range)
+            } {
+              gfx.setColor(color)
+              gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
+            }
+
             // highlighted range -- potentially from other snapshot
             doc_view.highlight_range match {
               case Some((range, color)) if line_range.overlaps(range) =>