more robust line_range, according to usual jEdit confusion at end of last line (see also 71c5d1f516c0);
--- a/src/Tools/jEdit/src/rich_text_area.scala Tue May 06 21:29:17 2014 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala Tue May 06 22:01:43 2014 +0200
@@ -277,7 +277,7 @@
for (i <- 0 until physical_lines.length) {
if (physical_lines(i) != -1) {
- val line_range = Text.Range(start(i), end(i))
+ val line_range = Text.Range(start(i), end(i) min buffer.getLength)
// line background color
for { (color, separator) <- rendering.line_background(line_range) }
@@ -456,7 +456,7 @@
for (i <- 0 until physical_lines.length) {
val line = physical_lines(i)
if (line != -1) {
- val line_range = Text.Range(start(i), end(i))
+ val line_range = Text.Range(start(i), end(i) min buffer.getLength)
// bullet bar
for {
@@ -501,7 +501,7 @@
val search_pattern = get_search_pattern()
for (i <- 0 until physical_lines.length) {
if (physical_lines(i) != -1) {
- val line_range = Text.Range(start(i), end(i))
+ val line_range = Text.Range(start(i), end(i) min buffer.getLength)
// foreground color
for {