# HG changeset patch
# User wenzelm
# Date 1479997314 -3600
# Node ID e6a3c55b929bf7447c14dc7ec9276dbf11a4d8f2
# Parent  49a29161d8efb27b3a833c080e2dee1de169b5cd
explicit option editor_generated_input_delay, which is more aggressive by default;

diff -r 49a29161d8ef -r e6a3c55b929b etc/options
--- a/etc/options	Thu Nov 24 11:33:55 2016 +0100
+++ b/etc/options	Thu Nov 24 15:21:54 2016 +0100
@@ -144,6 +144,9 @@
 public option editor_input_delay : real = 0.3
   -- "delay for user input (text edits, cursor movement etc.)"
 
+public option editor_generated_input_delay : real = 1.0
+  -- "delay for machine-generated input that may outperform user edits"
+
 public option editor_output_delay : real = 0.1
   -- "delay for prover output (markup, common messages etc.)"
 
diff -r 49a29161d8ef -r e6a3c55b929b src/Pure/PIDE/editor.scala
--- a/src/Pure/PIDE/editor.scala	Thu Nov 24 11:33:55 2016 +0100
+++ b/src/Pure/PIDE/editor.scala	Thu Nov 24 15:21:54 2016 +0100
@@ -12,7 +12,7 @@
   def session: Session
   def flush(hidden: Boolean = true): Unit
   def invoke(): Unit
-  def invoke_update(): Unit
+  def invoke_generated(): 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 49a29161d8ef -r e6a3c55b929b src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Thu Nov 24 11:33:55 2016 +0100
+++ b/src/Tools/jEdit/src/document_view.scala	Thu Nov 24 15:21:54 2016 +0100
@@ -111,7 +111,7 @@
       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
     {
       // no robust_body
-      PIDE.editor.invoke_update()
+      PIDE.editor.invoke_generated()
     }
   }
 
diff -r 49a29161d8ef -r e6a3c55b929b src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Thu Nov 24 11:33:55 2016 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Thu Nov 24 15:21:54 2016 +0100
@@ -44,14 +44,14 @@
     session.update(doc_blobs, edits)
   }
 
-  private val delay_flush =
+  private val delay1_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() }
+  private val delay2_flush =
+    GUI_Thread.delay_first(PIDE.options.seconds("editor_generated_input_delay")) { flush() }
 
-  def invoke(): Unit = delay_flush.invoke()
-  def invoke_update(): Unit = { delay_flush.invoke(); delay_update_flush.invoke() }
+  def invoke(): Unit = delay1_flush.invoke()
+  def invoke_generated(): Unit = { delay1_flush.invoke(); delay2_flush.invoke() }
 
   def stable_tip_version(): Option[Document.Version] =
     GUI_Thread.require {
diff -r 49a29161d8ef -r e6a3c55b929b src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Thu Nov 24 11:33:55 2016 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Thu Nov 24 15:21:54 2016 +0100
@@ -125,7 +125,7 @@
         else if (plugin != null) plugin.delay_init.invoke()
       }
 
-      PIDE.editor.invoke_update()
+      PIDE.editor.invoke_generated()
     }
   }