src/Pure/General/file_watcher.scala
changeset 64782 3f0bbb60859b
parent 64710 72ca4e5f976e
child 64807 7d556bb6046b
--- 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 {