src/Tools/jEdit/src/jedit_editor.scala
changeset 54461 6c360a6ade0e
parent 54325 2c4155003352
child 54521 744ea0025e11
     1.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Sun Nov 17 09:30:13 2013 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Sun Nov 17 16:02:06 2013 +0100
     1.3 @@ -36,6 +36,11 @@
     1.4      )
     1.5    }
     1.6  
     1.7 +  private val delay_flush =
     1.8 +    Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() }
     1.9 +
    1.10 +  def invoke(): Unit = Swing_Thread.require { delay_flush.invoke() }
    1.11 +
    1.12  
    1.13    /* current situation */
    1.14