src/Tools/jEdit/src/text_area_painter.scala
changeset 43451 be760a642d38
parent 43450 b6b09fc8d671
child 43505 0aca4edbfa99
     1.1 --- a/src/Tools/jEdit/src/text_area_painter.scala	Sat Jun 18 21:26:47 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/text_area_painter.scala	Sat Jun 18 22:01:22 2011 +0200
     1.3 @@ -219,7 +219,10 @@
     1.4  
     1.5          var x1 = x + w
     1.6          gfx.setFont(chunk_font)
     1.7 -        if (markup.isEmpty) gfx.drawString(chunk.str, x1, y)
     1.8 +        if (markup.isEmpty) {
     1.9 +          gfx.setColor(chunk_color)
    1.10 +          gfx.drawString(chunk.str, x1, y)
    1.11 +        }
    1.12          else {
    1.13            for {
    1.14              Text.Info(range, info) <-