1/*  Title:      Pure/General/file_watcher.scala
2    Author:     Makarius
3
4Watcher for file-system events.
5*/
6
7package isabelle
8
9
10import java.io.{File => JFile}
11import java.nio.file.FileSystems
12import java.nio.file.{WatchKey, WatchEvent, Path => JPath}
13import java.nio.file.StandardWatchEventKinds.{ENTRY_CREATE, ENTRY_DELETE, ENTRY_MODIFY}
14
15import scala.collection.JavaConverters
16
17
18class File_Watcher private[File_Watcher]  // dummy template
19{
20  def register(dir: JFile) { }
21  def register_parent(file: JFile) { }
22  def deregister(dir: JFile) { }
23  def purge(retain: Set[JFile]) { }
24  def shutdown() { }
25}
26
27object File_Watcher
28{
29  val none: File_Watcher = new File_Watcher
30  {
31    override def toString: String = "File_Watcher.none"
32  }
33
34  def apply(handle: Set[JFile] => Unit, delay: => Time = Time.seconds(0.5)): File_Watcher =
35    if (Platform.is_windows) none else new Impl(handle, delay)
36
37
38  /* proper implementation */
39
40  sealed case class State(
41    dirs: Map[JFile, WatchKey] = Map.empty,
42    changed: Set[JFile] = Set.empty)
43
44  class Impl private[File_Watcher](handle: Set[JFile] => Unit, delay: Time) extends File_Watcher
45  {
46    private val state = Synchronized(File_Watcher.State())
47    private val watcher = FileSystems.getDefault.newWatchService()
48
49    override def toString: String =
50      state.value.dirs.keySet.mkString("File_Watcher(", ", ", ")")
51
52
53    /* registered directories */
54
55    override def register(dir: JFile): Unit =
56      state.change(st =>
57        st.dirs.get(dir) match {
58          case Some(key) if key.isValid => st
59          case _ =>
60            val key = dir.toPath.register(watcher, ENTRY_CREATE, ENTRY_DELETE, ENTRY_MODIFY)
61            st.copy(dirs = st.dirs + (dir -> key))
62        })
63
64    override def register_parent(file: JFile): Unit =
65    {
66      val dir = file.getParentFile
67      if (dir != null && dir.isDirectory) register(dir)
68    }
69
70    override def deregister(dir: JFile): Unit =
71      state.change(st =>
72        st.dirs.get(dir) match {
73          case None => st
74          case Some(key) =>
75            key.cancel
76            st.copy(dirs = st.dirs - dir)
77        })
78
79    override def purge(retain: Set[JFile]): Unit =
80      state.change(st =>
81        st.copy(dirs = st.dirs --
82          (for ((dir, key) <- st.dirs.iterator if !retain(dir)) yield { key.cancel; dir })))
83
84
85    /* changed directory entries */
86
87    private val delay_changed = Standard_Thread.delay_last(delay)
88    {
89      val changed = state.change_result(st => (st.changed, st.copy(changed = Set.empty)))
90      handle(changed)
91    }
92
93    private val watcher_thread = Standard_Thread.fork("File_Watcher", daemon = true)
94    {
95      try {
96        while (true) {
97          val key = watcher.take
98          val has_changed =
99            state.change_result(st =>
100              {
101                val (remove, changed) =
102                  st.dirs.collectFirst({ case (dir, key1) if key == key1 => dir }) match {
103                    case Some(dir) =>
104                      val events =
105                        JavaConverters.collectionAsScalaIterable(
106                          key.pollEvents.asInstanceOf[java.util.List[WatchEvent[JPath]]])
107                      val remove = if (key.reset) None else Some(dir)
108                      val changed =
109                        (Set.empty[JFile] /: events.iterator) {
110                          case (set, event) => set + dir.toPath.resolve(event.context).toFile
111                        }
112                      (remove, changed)
113                    case None =>
114                      key.pollEvents
115                      key.reset
116                      (None, Set.empty[JFile])
117                  }
118                (changed.nonEmpty, st.copy(dirs = st.dirs -- remove, changed = st.changed ++ changed))
119              })
120          if (has_changed) delay_changed.invoke()
121        }
122      }
123      catch { case Exn.Interrupt() => }
124    }
125
126
127    /* shutdown */
128
129    override def shutdown()
130    {
131      watcher_thread.interrupt
132      watcher_thread.join
133      delay_changed.revoke
134    }
135  }
136}
137