# HG changeset patch # User wenzelm # Date 1308427282 -7200 # Node ID be760a642d385a10fec14a9dfa81509aa5ab17dc # Parent b6b09fc8d67149f121ff23c8ecba2667b452ae06 proper gfx.setColor; diff -r b6b09fc8d671 -r be760a642d38 src/Tools/jEdit/src/text_area_painter.scala --- a/src/Tools/jEdit/src/text_area_painter.scala Sat Jun 18 21:26:47 2011 +0200 +++ b/src/Tools/jEdit/src/text_area_painter.scala Sat Jun 18 22:01:22 2011 +0200 @@ -219,7 +219,10 @@ var x1 = x + w gfx.setFont(chunk_font) - if (markup.isEmpty) gfx.drawString(chunk.str, x1, y) + if (markup.isEmpty) { + gfx.setColor(chunk_color) + gfx.drawString(chunk.str, x1, y) + } else { for { Text.Info(range, info) <-