changeset 43414 | f0770743b7ec |
parent 43404 | c8369f3d88a1 |
child 43415 | 8f7494985093 |
--- a/src/Tools/jEdit/src/text_area_painter.scala Thu Jun 16 20:12:59 2011 +0200 +++ b/src/Tools/jEdit/src/text_area_painter.scala Thu Jun 16 22:05:40 2011 +0200 @@ -231,6 +231,7 @@ else { var x1 = x + w for (Text.Info(range, info) <- markup) { + // FIXME range check!? val str = chunk.str.substring(range.start - chunk_offset, range.stop - chunk_offset) gfx.setColor(info.getOrElse(chunk_color)) if (range.contains(caret_offset)) {