# HG changeset patch
# User wenzelm
# Date 1308394721 -7200
# Node ID 2fd41645813d952eb9cc1c71ba63e6a625a79a7d
# Parent  f67364f35789faf8eea5ba1595c843e347006164
tuned signature;

diff -r f67364f35789 -r 2fd41645813d src/Tools/jEdit/src/isabelle_markup.scala
--- a/src/Tools/jEdit/src/isabelle_markup.scala	Sat Jun 18 12:49:55 2011 +0200
+++ b/src/Tools/jEdit/src/isabelle_markup.scala	Sat Jun 18 12:58:41 2011 +0200
@@ -108,7 +108,7 @@
     case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color
   }
 
-  private val foreground_colors: Map[String, Color] =
+  private val text_colors: Map[String, Color] =
     Map(
       Markup.TCLASS -> get_color("red"),
       Markup.TFREE -> get_color("#A020F0"),
@@ -132,10 +132,10 @@
       Markup.ML_MALFORMED -> get_color("#FF6A6A"),
       Markup.ANTIQ -> get_color("blue"))
 
-  val foreground: Markup_Tree.Select[Color] =
+  val text_color: Markup_Tree.Select[Color] =
   {
     case Text.Info(_, XML.Elem(Markup(m, _), _))
-    if foreground_colors.isDefinedAt(m) => foreground_colors(m)
+    if text_colors.isDefinedAt(m) => text_colors(m)
   }
 
   private val tooltips: Map[String, String] =
diff -r f67364f35789 -r 2fd41645813d src/Tools/jEdit/src/text_area_painter.scala
--- a/src/Tools/jEdit/src/text_area_painter.scala	Sat Jun 18 12:49:55 2011 +0200
+++ b/src/Tools/jEdit/src/text_area_painter.scala	Sat Jun 18 12:58:41 2011 +0200
@@ -221,7 +221,7 @@
 
         val markup =
           for {
-            x <- painter_snapshot.select_markup(chunk_range)(Isabelle_Markup.foreground)
+            x <- painter_snapshot.select_markup(chunk_range)(Isabelle_Markup.text_color)
             y <- x.try_restrict(chunk_range)
           } yield y