src/Tools/jEdit/src/jedit_editor.scala
changeset 56770 e160ae47db94
parent 56729 1da2272a06a4
child 57611 b6256ea3b7c5
     1.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Apr 28 14:19:14 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Apr 28 14:41:49 2014 +0200
     1.3 @@ -34,7 +34,7 @@
     1.4    private val delay_flush =
     1.5      Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() }
     1.6  
     1.7 -  def invoke(): Unit = Swing_Thread.require { delay_flush.invoke() }
     1.8 +  def invoke(): Unit = delay_flush.invoke()
     1.9  
    1.10  
    1.11    /* current situation */