# HG changeset patch
# User wenzelm
# Date 1720689201 -7200
# Node ID 1638e980f73725503657d96937f20064d46dc040
# Parent  642e2de19d9589e0d04f746734515c150cde732d
clarified signature;

diff -r 642e2de19d95 -r 1638e980f737 src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Tue Jul 09 13:16:57 2024 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Thu Jul 11 11:13:21 2024 +0200
@@ -196,7 +196,7 @@
   private val delay_caret_update =
     Delay.last(PIDE.session.input_delay, gui = true) {
       session.caret_focus.post(Session.Caret_Focus)
-      JEdit_Lib.invalidate(text_area)
+      JEdit_Lib.invalidate_screen(text_area)
     }
 
   private val caret_listener = new CaretListener {
@@ -229,7 +229,7 @@
                    changed.commands.exists(snapshot.node.commands.contains)))
                 text_overview.foreach(_.invoke())
 
-              JEdit_Lib.invalidate(text_area)
+              JEdit_Lib.invalidate_screen(text_area)
             }
           }
         }
diff -r 642e2de19d95 -r 1638e980f737 src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Tue Jul 09 13:16:57 2024 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Thu Jul 11 11:13:21 2024 +0200
@@ -205,9 +205,11 @@
     }
   }
 
-  def invalidate(text_area: TextArea): Unit = {
+  def invalidate_screen(text_area: TextArea): Unit = {
     val visible_lines = text_area.getVisibleLines
-    if (visible_lines > 0) text_area.invalidateScreenLineRange(0, visible_lines)
+    if (visible_lines > 0) {
+      text_area.invalidateScreenLineRange(0, visible_lines)
+    }
   }