delay_first for machine generated editor events: avoid starvation, e.g. when operating on big sessions;

--- 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]

--- 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()
     }
   }
 

--- 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 {

--- 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()
     }
   }