equal
deleted
inserted
replaced
32 } |
32 } |
33 |
33 |
34 private val delay_flush = |
34 private val delay_flush = |
35 Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() } |
35 Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() } |
36 |
36 |
37 def invoke(): Unit = Swing_Thread.require { delay_flush.invoke() } |
37 def invoke(): Unit = delay_flush.invoke() |
38 |
38 |
39 |
39 |
40 /* current situation */ |
40 /* current situation */ |
41 |
41 |
42 override def current_context: View = |
42 override def current_context: View = |