tuned;
authorwenzelm
Wed, 04 Jan 2017 22:31:40 +0100
changeset 64782 3f0bbb60859b
parent 64781 31b5a28cadbc
child 64783 0be08e4cd0ec
tuned;
src/Pure/General/file_watcher.scala
src/Tools/VSCode/src/server.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 {
--- 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 =>
     }