equal
deleted
inserted
replaced
30 } |
30 } |
31 override def flush(): Unit = flush_edits() |
31 override def flush(): Unit = flush_edits() |
32 def purge() { flush_edits(purge = true) } |
32 def purge() { flush_edits(purge = true) } |
33 |
33 |
34 private val delay1_flush = |
34 private val delay1_flush = |
35 GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() } |
35 Delay.last(PIDE.options.seconds("editor_input_delay"), gui = true) { flush() } |
36 |
36 |
37 private val delay2_flush = |
37 private val delay2_flush = |
38 GUI_Thread.delay_first(PIDE.options.seconds("editor_generated_input_delay")) { flush() } |
38 Delay.first(PIDE.options.seconds("editor_generated_input_delay"), gui = true) { flush() } |
39 |
39 |
40 def invoke(): Unit = delay1_flush.invoke() |
40 def invoke(): Unit = delay1_flush.invoke() |
41 def invoke_generated(): Unit = { delay1_flush.invoke(); delay2_flush.invoke() } |
41 def invoke_generated(): Unit = { delay1_flush.invoke(); delay2_flush.invoke() } |
42 |
42 |
43 def shutdown(): Unit = |
43 def shutdown(): Unit = |