--- a/src/Tools/jEdit/src/jedit_lib.scala Thu Jul 11 13:33:58 2024 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala Thu Jul 11 15:51:19 2024 +0200
@@ -205,10 +205,12 @@
}
}
- def invalidate_screen(text_area: TextArea): Unit = {
+ def invalidate_screen(text_area: TextArea, start: Int = -1, end: Int = -1): Unit = {
val visible_lines = text_area.getVisibleLines
if (visible_lines > 0) {
- text_area.invalidateScreenLineRange(0, visible_lines)
+ val start_line = if (start >= 0) start else 0
+ val end_line = if (end >= 0) end else visible_lines
+ text_area.invalidateScreenLineRange(start_line, end_line)
}
}