src/Tools/VSCode/src/server.scala
changeset 65111 3224a6f7bd6b
parent 65107 70b0113fa4ef
child 65116 06d9bcb66ef3
--- a/src/Tools/VSCode/src/server.scala	Sun Mar 05 12:07:36 2017 +0100
+++ b/src/Tools/VSCode/src/server.scala	Sun Mar 05 13:34:35 2017 +0100
@@ -124,24 +124,32 @@
   private val file_watcher =
     File_Watcher(sync_documents(_), options.seconds("vscode_load_delay"))
 
-  private def sync_documents(changed: Set[JFile]): Unit =
-    if (resources.sync_models(changed)) delay_input.invoke()
+  private def close_document(file: JFile)
+  {
+    if (resources.close_model(file)) {
+      file_watcher.register_parent(file)
+      if (!sync_documents(Set(file))) {
+        delay_input.invoke()
+        delay_output.invoke()
+      }
+    }
+  }
+
+  private def sync_documents(changed: Set[JFile]): Boolean =
+    if (resources.sync_models(changed)) {
+      delay_input.invoke()
+      delay_output.invoke()
+      true
+    }
+    else false
 
   private def update_document(file: JFile, text: String)
   {
     resources.update_model(session, file, text)
     delay_input.invoke()
+    delay_output.invoke()
   }
 
-  private def close_document(file: JFile)
-  {
-    resources.close_model(file) match {
-      case Some(model) =>
-        file_watcher.register_parent(file)
-        sync_documents(Set(file))
-      case None =>
-    }
-  }
 
 
   /* output to client */