# HG changeset patch
# User wenzelm
# Date 1479914117 -3600
# Node ID 1aef5a0e18d7a970d804fba80fc66585c76b8de1
# Parent  8bf3d0553c35d7db42ec126ec9379ad5927f32bb
delay_first for machine generated editor events: avoid starvation, e.g. when operating on big sessions;

diff -r 8bf3d0553c35 -r 1aef5a0e18d7 src/Pure/PIDE/editor.scala
--- a/src/Pure/PIDE/editor.scala	Mon Nov 21 15:46:13 2016 +0100
+++ b/src/Pure/PIDE/editor.scala	Wed Nov 23 16:15:17 2016 +0100
@@ -12,6 +12,7 @@
   def session: Session
   def flush(hidden: Boolean = true): Unit
   def invoke(): Unit
+  def invoke_update(): Unit
   def current_context: Context
   def current_node(context: Context): Option[Document.Node.Name]
   def current_node_snapshot(context: Context): Option[Document.Snapshot]
diff -r 8bf3d0553c35 -r 1aef5a0e18d7 src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Mon Nov 21 15:46:13 2016 +0100
+++ b/src/Tools/jEdit/src/document_view.scala	Wed Nov 23 16:15:17 2016 +0100
@@ -111,7 +111,7 @@
       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
     {
       // no robust_body
-      PIDE.editor.invoke()
+      PIDE.editor.invoke_update()
     }
   }
 
diff -r 8bf3d0553c35 -r 1aef5a0e18d7 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Nov 21 15:46:13 2016 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Wed Nov 23 16:15:17 2016 +0100
@@ -47,7 +47,11 @@
   private val delay_flush =
     GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() }
 
+  private val delay_update_flush =
+    GUI_Thread.delay_first(Time.seconds(PIDE.options.real("editor_update_delay") * 3.0)) { flush() }
+
   def invoke(): Unit = delay_flush.invoke()
+  def invoke_update(): Unit = { delay_flush.invoke(); delay_update_flush.invoke() }
 
   def stable_tip_version(): Option[Document.Version] =
     GUI_Thread.require {
diff -r 8bf3d0553c35 -r 1aef5a0e18d7 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Mon Nov 21 15:46:13 2016 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Wed Nov 23 16:15:17 2016 +0100
@@ -125,7 +125,7 @@
         else if (plugin != null) plugin.delay_init.invoke()
       }
 
-      PIDE.editor.invoke()
+      PIDE.editor.invoke_update()
     }
   }