render snapshot.is_outdated in text overview, where other status information is shown already;
--- a/src/Tools/jEdit/src/document_view.scala Sat Nov 21 16:33:48 2015 +0100
+++ b/src/Tools/jEdit/src/document_view.scala Sat Nov 21 16:35:46 2015 +0100
@@ -201,7 +201,8 @@
private val main =
Session.Consumer[Any](getClass.getName) {
- case _: Session.Raw_Edits => overview.postpone()
+ case _: Session.Raw_Edits =>
+ overview.invoke()
case changed: Session.Commands_Changed =>
val buffer = model.buffer
--- a/src/Tools/jEdit/src/text_overview.scala Sat Nov 21 16:33:48 2015 +0100
+++ b/src/Tools/jEdit/src/text_overview.scala Sat Nov 21 16:35:46 2015 +0100
@@ -106,7 +106,6 @@
def invoke(): Unit = delay_refresh.invoke()
def revoke(): Unit = delay_refresh.revoke()
- def postpone(): Unit = { delay_refresh.postpone(PIDE.options.seconds("editor_input_delay")) }
private val delay_refresh =
GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay"), cancel _) {