# HG changeset patch
# User wenzelm
# Date 1375101801 -7200
# Node ID 9c28559e5fff0406f757e683298a865a2f13c074
# Parent  36c3c051b355640a4f3fcf36fef828a6b7e67865
back to model.update_perspective with delay (cf. a20631db9c8a);

diff -r 36c3c051b355 -r 9c28559e5fff src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Mon Jul 29 14:37:59 2013 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Mon Jul 29 14:43:21 2013 +0200
@@ -148,7 +148,7 @@
 
     def flush(): Unit = session.update(flushed_edits())
 
-    private val delay_flush =
+    val delay_flush =
       Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() }
 
     def +=(edit: Text.Edit)
@@ -172,7 +172,8 @@
   }
 
   def flushed_edits(): List[Document.Edit_Text] = pending_edits.flushed_edits()
-  def flush(): Unit = pending_edits.flush()
+
+  def update_perspective(): Unit = pending_edits.delay_flush.invoke()
 
 
   /* snapshot */
diff -r 36c3c051b355 -r 9c28559e5fff src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Mon Jul 29 14:37:59 2013 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Mon Jul 29 14:43:21 2013 +0200
@@ -100,7 +100,7 @@
       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
     {
       // no robust_body
-      model.flush()
+      model.update_perspective()
     }
   }