src/Tools/jEdit/src/rich_text_area.scala
changeset 49843 afddf4e26fac
parent 49730 e0d98ff3c0db
child 49941 f2db0596bd61
--- a/src/Tools/jEdit/src/rich_text_area.scala	Fri Oct 12 22:53:20 2012 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Fri Oct 12 23:38:48 2012 +0200
@@ -230,7 +230,7 @@
 
         for (i <- 0 until physical_lines.length) {
           if (physical_lines(i) != -1) {
-            val line_range = JEdit_Lib.proper_line_range(buffer, start(i), end(i))
+            val line_range = Text.Range(start(i), end(i))
 
             // line background color
             for { (color, separator) <- rendering.line_background(line_range) }
@@ -415,7 +415,7 @@
       robust_rendering { rendering =>
         for (i <- 0 until physical_lines.length) {
           if (physical_lines(i) != -1) {
-            val line_range = JEdit_Lib.proper_line_range(buffer, start(i), end(i))
+            val line_range = Text.Range(start(i), end(i))
 
             // foreground color
             for {