more robust line_range, according to usual jEdit confusion at end of last line (see also 71c5d1f516c0);
authorwenzelm
Tue, 06 May 2014 22:01:43 +0200
changeset 56884 7de69b35bdaf
parent 56883 38c6b70e5e53
child 56885 3020f6bbd119
more robust line_range, according to usual jEdit confusion at end of last line (see also 71c5d1f516c0);
src/Tools/jEdit/src/rich_text_area.scala
--- 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 {