equal
deleted
inserted
replaced
228 robust_rendering { rendering => |
228 robust_rendering { rendering => |
229 val ascent = text_area.getPainter.getFontMetrics.getAscent |
229 val ascent = text_area.getPainter.getFontMetrics.getAscent |
230 |
230 |
231 for (i <- 0 until physical_lines.length) { |
231 for (i <- 0 until physical_lines.length) { |
232 if (physical_lines(i) != -1) { |
232 if (physical_lines(i) != -1) { |
233 val line_range = JEdit_Lib.proper_line_range(buffer, start(i), end(i)) |
233 val line_range = Text.Range(start(i), end(i)) |
234 |
234 |
235 // line background color |
235 // line background color |
236 for { (color, separator) <- rendering.line_background(line_range) } |
236 for { (color, separator) <- rendering.line_background(line_range) } |
237 { |
237 { |
238 gfx.setColor(color) |
238 gfx.setColor(color) |
413 start: Array[Int], end: Array[Int], y: Int, line_height: Int) |
413 start: Array[Int], end: Array[Int], y: Int, line_height: Int) |
414 { |
414 { |
415 robust_rendering { rendering => |
415 robust_rendering { rendering => |
416 for (i <- 0 until physical_lines.length) { |
416 for (i <- 0 until physical_lines.length) { |
417 if (physical_lines(i) != -1) { |
417 if (physical_lines(i) != -1) { |
418 val line_range = JEdit_Lib.proper_line_range(buffer, start(i), end(i)) |
418 val line_range = Text.Range(start(i), end(i)) |
419 |
419 |
420 // foreground color |
420 // foreground color |
421 for { |
421 for { |
422 Text.Info(range, color) <- rendering.foreground(line_range) |
422 Text.Info(range, color) <- rendering.foreground(line_range) |
423 r <- JEdit_Lib.gfx_range(text_area, range) |
423 r <- JEdit_Lib.gfx_range(text_area, range) |