src/Tools/jEdit/src/text_area_painter.scala
changeset 43415 8f7494985093
parent 43414 f0770743b7ec
child 43419 6ed49c52d463
     1.1 --- a/src/Tools/jEdit/src/text_area_painter.scala	Thu Jun 16 22:05:40 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/text_area_painter.scala	Thu Jun 16 22:15:35 2011 +0200
     1.3 @@ -231,8 +231,11 @@
     1.4          else {
     1.5            var x1 = x + w
     1.6            for (Text.Info(range, info) <- markup) {
     1.7 -            // FIXME range check!?
     1.8 -            val str = chunk.str.substring(range.start - chunk_offset, range.stop - chunk_offset)
     1.9 +            // FIXME proper range!?
    1.10 +            val str =
    1.11 +              chunk.str.substring(
    1.12 +                (range.start - chunk_offset) max 0,
    1.13 +                (range.stop - chunk_offset) min chunk_length)
    1.14              gfx.setColor(info.getOrElse(chunk_color))
    1.15              if (range.contains(caret_offset)) {
    1.16                val astr = new AttributedString(str)