# HG changeset patch
# User wenzelm
# Date 1448120146 -3600
# Node ID 7feee72b58977cfa1739425b218216b25f795512
# Parent  a8fb3e379ba7e1ace769615152433246778da5ec
render snapshot.is_outdated in text overview, where other status information is shown already;

diff -r a8fb3e379ba7 -r 7feee72b5897 src/Tools/jEdit/src/document_view.scala
--- 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
diff -r a8fb3e379ba7 -r 7feee72b5897 src/Tools/jEdit/src/text_overview.scala
--- 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 _) {