# HG changeset patch
# User wenzelm
# Date 1720705879 -7200
# Node ID 2ee3d05afb22d98a2bc5c7530dbced534bc9a630
# Parent  a171f98c06a7aec568d28340b0e0e21c3d9f2a85
clarified signature: more arguments;

diff -r a171f98c06a7 -r 2ee3d05afb22 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)
     }
   }