equal
deleted
inserted
replaced
46 |
46 |
47 private val delay_flush = |
47 private val delay_flush = |
48 GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() } |
48 GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() } |
49 |
49 |
50 def invoke(): Unit = delay_flush.invoke() |
50 def invoke(): Unit = delay_flush.invoke() |
|
51 |
|
52 def stable_tip_version(): Option[Document.Version] = |
|
53 GUI_Thread.require { |
|
54 if (removed_nodes.isEmpty && PIDE.document_models().forall(_.is_stable)) |
|
55 session.current_state().stable_tip_version |
|
56 else None |
|
57 } |
51 |
58 |
52 |
59 |
53 /* current situation */ |
60 /* current situation */ |
54 |
61 |
55 override def current_context: View = |
62 override def current_context: View = |