explicit option editor_generated_input_delay, which is more aggressive by default;
authorwenzelm
Thu Nov 24 15:21:54 2016 +0100 (2016-11-24)
changeset 64524e6a3c55b929b
parent 64523 49a29161d8ef
child 64525 9c3da2276e19
explicit option editor_generated_input_delay, which is more aggressive by default;
etc/options
src/Pure/PIDE/editor.scala
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/jedit_editor.scala
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/etc/options	Thu Nov 24 11:33:55 2016 +0100
     1.2 +++ b/etc/options	Thu Nov 24 15:21:54 2016 +0100
     1.3 @@ -144,6 +144,9 @@
     1.4  public option editor_input_delay : real = 0.3
     1.5    -- "delay for user input (text edits, cursor movement etc.)"
     1.6  
     1.7 +public option editor_generated_input_delay : real = 1.0
     1.8 +  -- "delay for machine-generated input that may outperform user edits"
     1.9 +
    1.10  public option editor_output_delay : real = 0.1
    1.11    -- "delay for prover output (markup, common messages etc.)"
    1.12  
     2.1 --- a/src/Pure/PIDE/editor.scala	Thu Nov 24 11:33:55 2016 +0100
     2.2 +++ b/src/Pure/PIDE/editor.scala	Thu Nov 24 15:21:54 2016 +0100
     2.3 @@ -12,7 +12,7 @@
     2.4    def session: Session
     2.5    def flush(hidden: Boolean = true): Unit
     2.6    def invoke(): Unit
     2.7 -  def invoke_update(): Unit
     2.8 +  def invoke_generated(): Unit
     2.9    def current_context: Context
    2.10    def current_node(context: Context): Option[Document.Node.Name]
    2.11    def current_node_snapshot(context: Context): Option[Document.Snapshot]
     3.1 --- a/src/Tools/jEdit/src/document_view.scala	Thu Nov 24 11:33:55 2016 +0100
     3.2 +++ b/src/Tools/jEdit/src/document_view.scala	Thu Nov 24 15:21:54 2016 +0100
     3.3 @@ -111,7 +111,7 @@
     3.4        start: Array[Int], end: Array[Int], y: Int, line_height: Int)
     3.5      {
     3.6        // no robust_body
     3.7 -      PIDE.editor.invoke_update()
     3.8 +      PIDE.editor.invoke_generated()
     3.9      }
    3.10    }
    3.11  
     4.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Thu Nov 24 11:33:55 2016 +0100
     4.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Thu Nov 24 15:21:54 2016 +0100
     4.3 @@ -44,14 +44,14 @@
     4.4      session.update(doc_blobs, edits)
     4.5    }
     4.6  
     4.7 -  private val delay_flush =
     4.8 +  private val delay1_flush =
     4.9      GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() }
    4.10  
    4.11 -  private val delay_update_flush =
    4.12 -    GUI_Thread.delay_first(Time.seconds(PIDE.options.real("editor_update_delay") * 3.0)) { flush() }
    4.13 +  private val delay2_flush =
    4.14 +    GUI_Thread.delay_first(PIDE.options.seconds("editor_generated_input_delay")) { flush() }
    4.15  
    4.16 -  def invoke(): Unit = delay_flush.invoke()
    4.17 -  def invoke_update(): Unit = { delay_flush.invoke(); delay_update_flush.invoke() }
    4.18 +  def invoke(): Unit = delay1_flush.invoke()
    4.19 +  def invoke_generated(): Unit = { delay1_flush.invoke(); delay2_flush.invoke() }
    4.20  
    4.21    def stable_tip_version(): Option[Document.Version] =
    4.22      GUI_Thread.require {
     5.1 --- a/src/Tools/jEdit/src/plugin.scala	Thu Nov 24 11:33:55 2016 +0100
     5.2 +++ b/src/Tools/jEdit/src/plugin.scala	Thu Nov 24 15:21:54 2016 +0100
     5.3 @@ -125,7 +125,7 @@
     5.4          else if (plugin != null) plugin.delay_init.invoke()
     5.5        }
     5.6  
     5.7 -      PIDE.editor.invoke_update()
     5.8 +      PIDE.editor.invoke_generated()
     5.9      }
    5.10    }
    5.11