clarified signature: more arguments;
authorwenzelm
Thu, 11 Jul 2024 15:51:19 +0200
changeset 80554 2ee3d05afb22
parent 80553 a171f98c06a7
child 80555 a66a962b015b
clarified signature: more arguments;
src/Tools/jEdit/src/jedit_lib.scala
--- 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)
     }
   }