tuned --- following hints by IntelliJ IDEA;
authorwenzelm
Wed, 07 Apr 2021 18:04:30 +0200
changeset 73538 80db0d2759b5
parent 73537 56db8559eadb
child 73539 f800f8becbfb
tuned --- following hints by IntelliJ IDEA;
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)) {