tuned signature;
authorwenzelm
Sat, 18 Jun 2011 12:58:41 +0200
changeset 43434 2fd41645813d
parent 43433 f67364f35789
child 43435 ae6b0c3e58a8
tuned signature;
src/Tools/jEdit/src/isabelle_markup.scala
src/Tools/jEdit/src/text_area_painter.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] =
--- 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