src/Tools/jEdit/src/document_view.scala

   }
 
 
   /* text status overview left of scrollbar */
 
-  private object overview extends Text_Overview(this)
-  {
-    val delay_repaint =
-      GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { repaint() }
-  }
+  private val overview = new Text_Overview(this)
 
 
   /* main */
 
   private val main =
     Session.Consumer[Any](getClass.getName) {
-      case _: Session.Raw_Edits =>
-        overview.delay_repaint.postpone(PIDE.options.seconds("editor_input_delay"))
+      case _: Session.Raw_Edits => overview.postpone()
 
       case changed: Session.Commands_Changed =>
         val buffer = model.buffer
         GUI_Thread.later {
           JEdit_Lib.buffer_lock(buffer) {

                 snapshot.load_commands.exists(changed.commands.contains)
 
               if (changed.assignment || load_changed ||
                   (changed.nodes.contains(model.node_name) &&
                    changed.commands.exists(snapshot.node.commands.contains)))
-                overview.delay_repaint.invoke()
+                overview.invoke()
 
               val visible_lines = text_area.getVisibleLines
               if (visible_lines > 0) {
                 if (changed.assignment || load_changed)
                   text_area.invalidateScreenLineRange(0, visible_lines)

 
     session.raw_edits -= main
     session.commands_changed -= main
     Isabelle.structure_matchers(JEdit_Lib.buffer_mode(text_area.getBuffer)).
       foreach(text_area.removeStructureMatcher(_))
-    text_area.removeLeftOfScrollBar(overview); overview.delay_repaint.revoke()
+    text_area.removeLeftOfScrollBar(overview); overview.revoke()
     text_area.removeCaretListener(caret_listener); delay_caret_update.revoke()
     text_area.removeKeyListener(key_listener)
     text_area.getGutter.removeExtension(gutter_painter)
     rich_text_area.deactivate()
     painter.removeExtension(update_view)