src/Tools/jEdit/src/text_area_painter.scala
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)) {