# HG changeset patch
# User wenzelm
# Date 1617811470 -7200
# Node ID 80db0d2759b54c8ff03b7a117c3084996b1c95d6
# Parent  56db8559eadb0c2577fb1c4c5d36510cf09b42f9
tuned --- following hints by IntelliJ IDEA;

diff -r 56db8559eadb -r 80db0d2759b5 src/Tools/VSCode/src/language_server.scala
--- a/src/Tools/VSCode/src/language_server.scala	Wed Apr 07 11:05:00 2021 +0200
+++ b/src/Tools/VSCode/src/language_server.scala	Wed Apr 07 18:04:30 2021 +0200
@@ -127,6 +127,9 @@
 
   /* input from client or file-system */
 
+  private val file_watcher: File_Watcher =
+    File_Watcher(sync_documents, options.seconds("vscode_load_delay"))
+
   private val delay_input: Delay =
     Delay.last(options.seconds("vscode_input_delay"), channel.Error_Logger)
     { resources.flush_input(session, channel) }
@@ -139,9 +142,6 @@
       if (invoke_load) delay_load.invoke()
     }
 
-  private val file_watcher =
-    File_Watcher(sync_documents, options.seconds("vscode_load_delay"))
-
   private def close_document(file: JFile): Unit =
   {
     if (resources.close_model(file)) {