# HG changeset patch
# User wenzelm
# Date 1662212366 -7200
# Node ID c90799513ed0c48a085e055573eb7d6e2b790822
# Parent  b80f33e5323fd66407558abc5ea3e17df8774d2e
tuned signature;

diff -r b80f33e5323f -r c90799513ed0 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Fri Sep 02 23:42:09 2022 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Sat Sep 03 15:39:26 2022 +0200
@@ -30,19 +30,19 @@
   override def flush(): Unit = flush_edits()
   def purge(): Unit = flush_edits(purge = true)
 
-  private val delay1_flush =
+  private val delay_input: Delay =
     Delay.last(PIDE.options.seconds("editor_input_delay"), gui = true) { flush() }
 
-  private val delay2_flush =
+  private val delay_generated_input: Delay =
     Delay.first(PIDE.options.seconds("editor_generated_input_delay"), gui = true) { flush() }
 
-  def invoke(): Unit = delay1_flush.invoke()
-  def invoke_generated(): Unit = { delay1_flush.invoke(); delay2_flush.invoke() }
+  def invoke(): Unit = delay_input.invoke()
+  def invoke_generated(): Unit = { delay_input.invoke(); delay_generated_input.invoke() }
 
   def shutdown(): Unit =
     GUI_Thread.require {
-      delay1_flush.revoke()
-      delay2_flush.revoke()
+      delay_input.revoke()
+      delay_generated_input.revoke()
       Document_Model.flush_edits(hidden = false, purge = false)
     }