render snapshot.is_outdated in text overview, where other status information is shown already;
authorwenzelm
Sat, 21 Nov 2015 16:35:46 +0100
changeset 61723 7feee72b5897
parent 61722 a8fb3e379ba7
child 61724 4bfcc09a33e8
render snapshot.is_outdated in text overview, where other status information is shown already;
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/text_overview.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
--- 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 _) {