src/Tools/jEdit/src/jedit_editor.scala

--- a/src/Tools/jEdit/src/jedit_editor.scala	Sun Nov 17 09:30:13 2013 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Sun Nov 17 16:02:06 2013 +0100
@@ -36,6 +36,11 @@
     )
   }
 
+  private val delay_flush =
+    Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() }
+
+  def invoke(): Unit = Swing_Thread.require { delay_flush.invoke() }
+
 
   /* current situation */