src/Tools/jEdit/src/jedit_editor.scala
changeset 64521 1aef5a0e18d7
parent 62248 dca0bac351b2
child 64524 e6a3c55b929b
     1.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Nov 21 15:46:13 2016 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Wed Nov 23 16:15:17 2016 +0100
     1.3 @@ -47,7 +47,11 @@
     1.4    private val delay_flush =
     1.5      GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() }
     1.6  
     1.7 +  private val delay_update_flush =
     1.8 +    GUI_Thread.delay_first(Time.seconds(PIDE.options.real("editor_update_delay") * 3.0)) { flush() }
     1.9 +
    1.10    def invoke(): Unit = delay_flush.invoke()
    1.11 +  def invoke_update(): Unit = { delay_flush.invoke(); delay_update_flush.invoke() }
    1.12  
    1.13    def stable_tip_version(): Option[Document.Version] =
    1.14      GUI_Thread.require {