src/Tools/VSCode/src/server.scala
changeset 66676 39db5bb7eb0a
parent 66675 6f4613dbfef6
child 66677 fa70edfcb6fa
     1.1 --- a/src/Tools/VSCode/src/server.scala	Mon Sep 18 18:11:21 2017 +0200
     1.2 +++ b/src/Tools/VSCode/src/server.scala	Mon Sep 18 18:19:06 2017 +0200
     1.3 @@ -123,7 +123,7 @@
     1.4  
     1.5    private val delay_input: Standard_Thread.Delay =
     1.6      Standard_Thread.delay_last(options.seconds("vscode_input_delay"), channel.Error_Logger)
     1.7 -    { resources.flush_input(session) }
     1.8 +    { resources.flush_input(session, channel) }
     1.9  
    1.10    private val delay_load: Standard_Thread.Delay =
    1.11      Standard_Thread.delay_last(options.seconds("vscode_load_delay"), channel.Error_Logger) {
    1.12 @@ -487,7 +487,7 @@
    1.13      /* session */
    1.14  
    1.15      override def session: Session = server.session
    1.16 -    override def flush(): Unit = resources.flush_input(session)
    1.17 +    override def flush(): Unit = resources.flush_input(session, channel)
    1.18      override def invoke(): Unit = delay_input.invoke()
    1.19  
    1.20