src/Tools/VSCode/src/server.scala
changeset 64684 fe2c9c215b36
parent 64683 c0c09b6dfbe0
child 64687 04806ad1e43a
     1.1 --- a/src/Tools/VSCode/src/server.scala	Wed Dec 28 17:26:38 2016 +0100
     1.2 +++ b/src/Tools/VSCode/src/server.scala	Wed Dec 28 17:35:12 2016 +0100
     1.3 @@ -118,7 +118,7 @@
     1.4    /* input from client */
     1.5  
     1.6    private val delay_input =
     1.7 -    Standard_Thread.delay_last(options.seconds("editor_input_delay")) {
     1.8 +    Standard_Thread.delay_last(options.seconds("vscode_input_delay")) {
     1.9        state.change(st =>
    1.10          {
    1.11            val changed = (for { entry <- st.models.iterator if entry._2.changed } yield entry).toList
    1.12 @@ -151,7 +151,7 @@
    1.13      }
    1.14  
    1.15    private val delay_output =
    1.16 -    Standard_Thread.delay_last(options.seconds("editor_update_delay")) {
    1.17 +    Standard_Thread.delay_last(options.seconds("vscode_output_delay")) {
    1.18        state.change(st =>
    1.19          {
    1.20            val changed_iterator =