src/Tools/jEdit/src/text_area_painter.scala
changeset 43506 bf7400573617
parent 43505 0aca4edbfa99
child 43759 d93a69672362
equal deleted inserted replaced
43505:0aca4edbfa99 43506:bf7400573617
   196     var w = 0.0f
   196     var w = 0.0f
   197     var chunk = head
   197     var chunk = head
   198     while (chunk != null) {
   198     while (chunk != null) {
   199       val chunk_offset = line_start + chunk.offset
   199       val chunk_offset = line_start + chunk.offset
   200       if (x + w + chunk.width > clip_rect.x &&
   200       if (x + w + chunk.width > clip_rect.x &&
   201           x + w < clip_rect.x + clip_rect.width &&
   201           x + w < clip_rect.x + clip_rect.width && chunk.accessable)
   202           chunk.accessable && chunk.visible)
       
   203       {
   202       {
   204         val chunk_range = Text.Range(chunk_offset, chunk_offset + chunk.length)
   203         val chunk_range = Text.Range(chunk_offset, chunk_offset + chunk.length)
   205         val chunk_font = chunk.style.getFont
   204         val chunk_font = chunk.style.getFont
   206         val chunk_color = chunk.style.getForegroundColor
   205         val chunk_color = chunk.style.getForegroundColor
   207 
   206