changeset 50207 | 54be125d8cdc |
parent 50205 | 788c8263e634 |
child 50344 | 608265769ce0 |
--- a/src/Tools/jEdit/src/document_model.scala Sun Nov 25 21:10:29 2012 +0100 +++ b/src/Tools/jEdit/src/document_model.scala Sun Nov 25 21:23:20 2012 +0100 @@ -115,7 +115,7 @@ } private val delay_flush = - Swing_Thread.delay_last(Time.seconds(PIDE.options.real("editor_input_delay"))) { flush() } + Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() } def +=(edit: Text.Edit) {