src/Tools/jEdit/src/document_view.scala

     Swing_Thread.delay_last(session.input_delay) {
       session.caret_focus.event(Session.Caret_Focus)
     }
 
   private val caret_listener = new CaretListener {
-    override def caretUpdate(e: CaretEvent) { delay_caret_update(true) }
+    override def caretUpdate(e: CaretEvent) { delay_caret_update.invoke() }
   }
 
 
   /* text status overview left of scrollbar */
 

                 val snapshot = model.snapshot()
 
                 if (changed.assignment ||
                     (changed.nodes.contains(model.name) &&
                      changed.commands.exists(snapshot.node.commands.contains)))
-                  overview.delay_repaint(true)
+                  overview.delay_repaint.invoke()
 
                 visible_range() match {
                   case Some(visible) =>
                     if (changed.assignment) invalidate_range(visible)
                     else {

     session.global_settings -= main_actor
     text_area.removeFocusListener(focus_listener)
     text_area.getView.removeWindowListener(window_listener)
     painter.removeMouseMotionListener(mouse_motion_listener)
     painter.removeMouseListener(mouse_listener)
-    text_area.removeCaretListener(caret_listener); delay_caret_update(false)
-    text_area.removeLeftOfScrollBar(overview); overview.delay_repaint(false)
+    text_area.removeCaretListener(caret_listener); delay_caret_update.revoke()
+    text_area.removeLeftOfScrollBar(overview); overview.delay_repaint.revoke()
     text_area.getGutter.removeExtension(gutter_painter)
     text_area_painter.deactivate()
     painter.removeExtension(tooltip_painter)
     painter.removeExtension(update_perspective)
     exit_popup()