--- 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 {