| changeset 61723 | 7feee72b5897 |
| parent 61561 | f35786faee6c |
| child 61747 | a870098fc27e |
--- a/src/Tools/jEdit/src/text_overview.scala Sat Nov 21 16:33:48 2015 +0100 +++ b/src/Tools/jEdit/src/text_overview.scala Sat Nov 21 16:35:46 2015 +0100 @@ -106,7 +106,6 @@ def invoke(): Unit = delay_refresh.invoke() def revoke(): Unit = delay_refresh.revoke() - def postpone(): Unit = { delay_refresh.postpone(PIDE.options.seconds("editor_input_delay")) } private val delay_refresh = GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay"), cancel _) {