src/Tools/jEdit/src/text_area_painter.scala
changeset 49408 3cfc114acd05
parent 49407 215ba6884bdf
child 49409 7140a738aa49
--- a/src/Tools/jEdit/src/text_area_painter.scala	Mon Sep 17 17:56:10 2012 +0200
+++ b/src/Tools/jEdit/src/text_area_painter.scala	Mon Sep 17 18:06:34 2012 +0200
@@ -119,7 +119,7 @@
 
         for (i <- 0 until physical_lines.length) {
           if (physical_lines(i) != -1) {
-            val line_range = doc_view.proper_line_range(start(i), end(i))
+            val line_range = JEdit_Lib.proper_line_range(buffer, start(i), end(i))
 
             // background color (1)
             for {
@@ -286,7 +286,7 @@
       robust_rendering { rendering =>
         for (i <- 0 until physical_lines.length) {
           if (physical_lines(i) != -1) {
-            val line_range = doc_view.proper_line_range(start(i), end(i))
+            val line_range = JEdit_Lib.proper_line_range(buffer, start(i), end(i))
 
             // foreground color
             for {