delay_first for machine generated editor events: avoid starvation, e.g. when operating on big sessions;
authorwenzelm
Wed Nov 23 16:15:17 2016 +0100 (2016-11-23)
changeset 645211aef5a0e18d7
parent 64520 8bf3d0553c35
child 64522 b66f8caf86b6
delay_first for machine generated editor events: avoid starvation, e.g. when operating on big sessions;
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/src/Pure/PIDE/editor.scala	Mon Nov 21 15:46:13 2016 +0100
     1.2 +++ b/src/Pure/PIDE/editor.scala	Wed Nov 23 16:15:17 2016 +0100
     1.3 @@ -12,6 +12,7 @@
     1.4    def session: Session
     1.5    def flush(hidden: Boolean = true): Unit
     1.6    def invoke(): Unit
     1.7 +  def invoke_update(): Unit
     1.8    def current_context: Context
     1.9    def current_node(context: Context): Option[Document.Node.Name]
    1.10    def current_node_snapshot(context: Context): Option[Document.Snapshot]
     2.1 --- a/src/Tools/jEdit/src/document_view.scala	Mon Nov 21 15:46:13 2016 +0100
     2.2 +++ b/src/Tools/jEdit/src/document_view.scala	Wed Nov 23 16:15:17 2016 +0100
     2.3 @@ -111,7 +111,7 @@
     2.4        start: Array[Int], end: Array[Int], y: Int, line_height: Int)
     2.5      {
     2.6        // no robust_body
     2.7 -      PIDE.editor.invoke()
     2.8 +      PIDE.editor.invoke_update()
     2.9      }
    2.10    }
    2.11  
     3.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Nov 21 15:46:13 2016 +0100
     3.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Wed Nov 23 16:15:17 2016 +0100
     3.3 @@ -47,7 +47,11 @@
     3.4    private val delay_flush =
     3.5      GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() }
     3.6  
     3.7 +  private val delay_update_flush =
     3.8 +    GUI_Thread.delay_first(Time.seconds(PIDE.options.real("editor_update_delay") * 3.0)) { flush() }
     3.9 +
    3.10    def invoke(): Unit = delay_flush.invoke()
    3.11 +  def invoke_update(): Unit = { delay_flush.invoke(); delay_update_flush.invoke() }
    3.12  
    3.13    def stable_tip_version(): Option[Document.Version] =
    3.14      GUI_Thread.require {
     4.1 --- a/src/Tools/jEdit/src/plugin.scala	Mon Nov 21 15:46:13 2016 +0100
     4.2 +++ b/src/Tools/jEdit/src/plugin.scala	Wed Nov 23 16:15:17 2016 +0100
     4.3 @@ -125,7 +125,7 @@
     4.4          else if (plugin != null) plugin.delay_init.invoke()
     4.5        }
     4.6  
     4.7 -      PIDE.editor.invoke()
     4.8 +      PIDE.editor.invoke_update()
     4.9      }
    4.10    }
    4.11