# HG changeset patch
# User wenzelm
# Date 1624714407 -7200
# Node ID b1272ec715680e0a4cd7d3c3e4ed795344edb139
# Parent  9ce206f6e8c67544e02c4325034bc96f420c37cd
tuned signature;

diff -r 9ce206f6e8c6 -r b1272ec71568 src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Sat Jun 26 15:32:08 2021 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Sat Jun 26 15:33:27 2021 +0200
@@ -176,7 +176,7 @@
     def update_rendering(r: JEdit_Rendering, range: Text.Range): Unit =
       update(rendering(r)(range))
 
-    def reset: Unit = update(None)
+    def reset(): Unit = update(None)
   }
 
   // owned by GUI thread
@@ -195,7 +195,7 @@
 
   private val active_areas =
     List((highlight_area, true), (hyperlink_area, true), (active_area, false))
-  def active_reset(): Unit = active_areas.foreach(_._1.reset)
+  def active_reset(): Unit = active_areas.foreach(_._1.reset())
 
   private def area_active(): Boolean =
     active_areas.exists({ case (area, _) => area.is_active })
@@ -273,7 +273,7 @@
                 {
                   if (control == require_control && !rendering.snapshot.is_outdated)
                     area.update_rendering(rendering, range)
-                  else area.reset
+                  else area.reset()
                 }
             }
           }