src/Tools/jEdit/src/text_area_painter.scala
changeset 43434 2fd41645813d
parent 43428 b41dea5772c6
child 43435 ae6b0c3e58a8
     1.1 --- a/src/Tools/jEdit/src/text_area_painter.scala	Sat Jun 18 12:49:55 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/text_area_painter.scala	Sat Jun 18 12:58:41 2011 +0200
     1.3 @@ -221,7 +221,7 @@
     1.4  
     1.5          val markup =
     1.6            for {
     1.7 -            x <- painter_snapshot.select_markup(chunk_range)(Isabelle_Markup.foreground)
     1.8 +            x <- painter_snapshot.select_markup(chunk_range)(Isabelle_Markup.text_color)
     1.9              y <- x.try_restrict(chunk_range)
    1.10            } yield y
    1.11