# HG changeset patch
# User wenzelm
# Date 1483565500 -3600
# Node ID 3f0bbb60859b6060dffd3a54fa6ec14f6d22b689
# Parent  31b5a28cadbc054a51244af93d251ba973cd8e63
tuned;

diff -r 31b5a28cadbc -r 3f0bbb60859b src/Pure/General/file_watcher.scala
--- a/src/Pure/General/file_watcher.scala	Wed Jan 04 21:29:19 2017 +0100
+++ b/src/Pure/General/file_watcher.scala	Wed Jan 04 22:31:40 2017 +0100
@@ -45,6 +45,12 @@
           st.copy(dirs = st.dirs + (dir -> key))
       })
 
+  def register_parent(file: JFile): Unit =
+  {
+    val dir = file.getParentFile
+    if (dir != null && dir.isDirectory) register(dir)
+  }
+
   def deregister(dir: JFile): Unit =
     state.change(st =>
       st.dirs.get(dir) match {
diff -r 31b5a28cadbc -r 3f0bbb60859b src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Wed Jan 04 21:29:19 2017 +0100
+++ b/src/Tools/VSCode/src/server.scala	Wed Jan 04 22:31:40 2017 +0100
@@ -134,8 +134,7 @@
   {
     resources.close_model(file) match {
       case Some(model) =>
-        val dir = file.getParentFile
-        if (dir != null && dir.isDirectory) watcher.register(dir)
+        watcher.register_parent(file)
         sync_documents(Set(file))
       case None =>
     }