tuned signature;
authorwenzelm
Sat Jun 18 12:58:41 2011 +0200 (2011-06-18)
changeset 434342fd41645813d
parent 43433 f67364f35789
child 43435 ae6b0c3e58a8
tuned signature;
src/Tools/jEdit/src/isabelle_markup.scala
src/Tools/jEdit/src/text_area_painter.scala
     1.1 --- a/src/Tools/jEdit/src/isabelle_markup.scala	Sat Jun 18 12:49:55 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/isabelle_markup.scala	Sat Jun 18 12:58:41 2011 +0200
     1.3 @@ -108,7 +108,7 @@
     1.4      case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color
     1.5    }
     1.6  
     1.7 -  private val foreground_colors: Map[String, Color] =
     1.8 +  private val text_colors: Map[String, Color] =
     1.9      Map(
    1.10        Markup.TCLASS -> get_color("red"),
    1.11        Markup.TFREE -> get_color("#A020F0"),
    1.12 @@ -132,10 +132,10 @@
    1.13        Markup.ML_MALFORMED -> get_color("#FF6A6A"),
    1.14        Markup.ANTIQ -> get_color("blue"))
    1.15  
    1.16 -  val foreground: Markup_Tree.Select[Color] =
    1.17 +  val text_color: Markup_Tree.Select[Color] =
    1.18    {
    1.19      case Text.Info(_, XML.Elem(Markup(m, _), _))
    1.20 -    if foreground_colors.isDefinedAt(m) => foreground_colors(m)
    1.21 +    if text_colors.isDefinedAt(m) => text_colors(m)
    1.22    }
    1.23  
    1.24    private val tooltips: Map[String, String] =
     2.1 --- a/src/Tools/jEdit/src/text_area_painter.scala	Sat Jun 18 12:49:55 2011 +0200
     2.2 +++ b/src/Tools/jEdit/src/text_area_painter.scala	Sat Jun 18 12:58:41 2011 +0200
     2.3 @@ -221,7 +221,7 @@
     2.4  
     2.5          val markup =
     2.6            for {
     2.7 -            x <- painter_snapshot.select_markup(chunk_range)(Isabelle_Markup.foreground)
     2.8 +            x <- painter_snapshot.select_markup(chunk_range)(Isabelle_Markup.text_color)
     2.9              y <- x.try_restrict(chunk_range)
    2.10            } yield y
    2.11