src/Tools/jEdit/src/text_overview.scala
changeset 61723 7feee72b5897
parent 61561 f35786faee6c
child 61747 a870098fc27e
equal deleted inserted replaced
61722:a8fb3e379ba7 61723:7feee72b5897
   104   private var future_refresh: Option[Future[Unit]] = None
   104   private var future_refresh: Option[Future[Unit]] = None
   105   private def cancel(): Unit = future_refresh.map(_.cancel)
   105   private def cancel(): Unit = future_refresh.map(_.cancel)
   106 
   106 
   107   def invoke(): Unit = delay_refresh.invoke()
   107   def invoke(): Unit = delay_refresh.invoke()
   108   def revoke(): Unit = delay_refresh.revoke()
   108   def revoke(): Unit = delay_refresh.revoke()
   109   def postpone(): Unit = { delay_refresh.postpone(PIDE.options.seconds("editor_input_delay")) }
       
   110 
   109 
   111   private val delay_refresh =
   110   private val delay_refresh =
   112     GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay"), cancel _) {
   111     GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay"), cancel _) {
   113       doc_view.rich_text_area.robust_body(()) {
   112       doc_view.rich_text_area.robust_body(()) {
   114         JEdit_Lib.buffer_lock(buffer) {
   113         JEdit_Lib.buffer_lock(buffer) {