--- 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)) {