src/Tools/jEdit/src/document_view.scala
changeset 61195 42419fe6f660
parent 59129 6959ceb53ac8
child 61723 7feee72b5897
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Sat Sep 19 20:31:57 2015 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Sat Sep 19 20:38:28 2015 +0200
     1.3 @@ -194,19 +194,14 @@
     1.4  
     1.5    /* text status overview left of scrollbar */
     1.6  
     1.7 -  private object overview extends Text_Overview(this)
     1.8 -  {
     1.9 -    val delay_repaint =
    1.10 -      GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { repaint() }
    1.11 -  }
    1.12 +  private val overview = new Text_Overview(this)
    1.13  
    1.14  
    1.15    /* main */
    1.16  
    1.17    private val main =
    1.18      Session.Consumer[Any](getClass.getName) {
    1.19 -      case _: Session.Raw_Edits =>
    1.20 -        overview.delay_repaint.postpone(PIDE.options.seconds("editor_input_delay"))
    1.21 +      case _: Session.Raw_Edits => overview.postpone()
    1.22  
    1.23        case changed: Session.Commands_Changed =>
    1.24          val buffer = model.buffer
    1.25 @@ -221,7 +216,7 @@
    1.26                if (changed.assignment || load_changed ||
    1.27                    (changed.nodes.contains(model.node_name) &&
    1.28                     changed.commands.exists(snapshot.node.commands.contains)))
    1.29 -                overview.delay_repaint.invoke()
    1.30 +                overview.invoke()
    1.31  
    1.32                val visible_lines = text_area.getVisibleLines
    1.33                if (visible_lines > 0) {
    1.34 @@ -275,7 +270,7 @@
    1.35      session.commands_changed -= main
    1.36      Isabelle.structure_matchers(JEdit_Lib.buffer_mode(text_area.getBuffer)).
    1.37        foreach(text_area.removeStructureMatcher(_))
    1.38 -    text_area.removeLeftOfScrollBar(overview); overview.delay_repaint.revoke()
    1.39 +    text_area.removeLeftOfScrollBar(overview); overview.revoke()
    1.40      text_area.removeCaretListener(caret_listener); delay_caret_update.revoke()
    1.41      text_area.removeKeyListener(key_listener)
    1.42      text_area.getGutter.removeExtension(gutter_painter)