render snapshot.is_outdated in text overview, where other status information is shown already;
authorwenzelm
Sat Nov 21 16:35:46 2015 +0100 (2015-11-21)
changeset 617237feee72b5897
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
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Sat Nov 21 16:33:48 2015 +0100
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Sat Nov 21 16:35:46 2015 +0100
     1.3 @@ -201,7 +201,8 @@
     1.4  
     1.5    private val main =
     1.6      Session.Consumer[Any](getClass.getName) {
     1.7 -      case _: Session.Raw_Edits => overview.postpone()
     1.8 +      case _: Session.Raw_Edits =>
     1.9 +        overview.invoke()
    1.10  
    1.11        case changed: Session.Commands_Changed =>
    1.12          val buffer = model.buffer
     2.1 --- a/src/Tools/jEdit/src/text_overview.scala	Sat Nov 21 16:33:48 2015 +0100
     2.2 +++ b/src/Tools/jEdit/src/text_overview.scala	Sat Nov 21 16:35:46 2015 +0100
     2.3 @@ -106,7 +106,6 @@
     2.4  
     2.5    def invoke(): Unit = delay_refresh.invoke()
     2.6    def revoke(): Unit = delay_refresh.revoke()
     2.7 -  def postpone(): Unit = { delay_refresh.postpone(PIDE.options.seconds("editor_input_delay")) }
     2.8  
     2.9    private val delay_refresh =
    2.10      GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay"), cancel _) {