--- 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 =>
}