back to model.update_perspective with delay (cf. a20631db9c8a);
authorwenzelm
Mon Jul 29 14:43:21 2013 +0200 (2013-07-29)
changeset 527679c28559e5fff
parent 52766 36c3c051b355
child 52768 1df3e32af79a
back to model.update_perspective with delay (cf. a20631db9c8a);
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/document_view.scala
     1.1 --- a/src/Tools/jEdit/src/document_model.scala	Mon Jul 29 14:37:59 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_model.scala	Mon Jul 29 14:43:21 2013 +0200
     1.3 @@ -148,7 +148,7 @@
     1.4  
     1.5      def flush(): Unit = session.update(flushed_edits())
     1.6  
     1.7 -    private val delay_flush =
     1.8 +    val delay_flush =
     1.9        Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() }
    1.10  
    1.11      def +=(edit: Text.Edit)
    1.12 @@ -172,7 +172,8 @@
    1.13    }
    1.14  
    1.15    def flushed_edits(): List[Document.Edit_Text] = pending_edits.flushed_edits()
    1.16 -  def flush(): Unit = pending_edits.flush()
    1.17 +
    1.18 +  def update_perspective(): Unit = pending_edits.delay_flush.invoke()
    1.19  
    1.20  
    1.21    /* snapshot */
     2.1 --- a/src/Tools/jEdit/src/document_view.scala	Mon Jul 29 14:37:59 2013 +0200
     2.2 +++ b/src/Tools/jEdit/src/document_view.scala	Mon Jul 29 14:43:21 2013 +0200
     2.3 @@ -100,7 +100,7 @@
     2.4        start: Array[Int], end: Array[Int], y: Int, line_height: Int)
     2.5      {
     2.6        // no robust_body
     2.7 -      model.flush()
     2.8 +      model.update_perspective()
     2.9      }
    2.10    }
    2.11