diff -r a8fb3e379ba7 -r 7feee72b5897 src/Tools/jEdit/src/text_overview.scala
--- 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 _) {