64699
|
1 |
/* Title: Pure/General/file_watcher.scala
|
|
2 |
Author: Makarius
|
|
3 |
|
|
4 |
Watcher for file-system events.
|
|
5 |
*/
|
|
6 |
|
|
7 |
package isabelle
|
|
8 |
|
|
9 |
|
|
10 |
import java.io.{File => JFile}
|
|
11 |
import java.nio.file.FileSystems
|
|
12 |
import java.nio.file.{WatchKey, WatchEvent, Path => JPath}
|
|
13 |
import java.nio.file.StandardWatchEventKinds.{ENTRY_CREATE, ENTRY_DELETE, ENTRY_MODIFY}
|
|
14 |
|
|
15 |
import scala.collection.JavaConversions
|
|
16 |
|
|
17 |
|
|
18 |
object File_Watcher
|
|
19 |
{
|
|
20 |
def apply(handle: Set[JFile] => Unit, delay: => Time = Time.seconds(0.5)): File_Watcher =
|
|
21 |
new File_Watcher(handle, delay)
|
|
22 |
|
|
23 |
|
|
24 |
/* internal state */
|
|
25 |
|
|
26 |
sealed case class State(
|
|
27 |
dirs: Map[JFile, WatchKey] = Map.empty,
|
|
28 |
changed: Set[JFile] = Set.empty)
|
|
29 |
}
|
|
30 |
|
|
31 |
class File_Watcher private(handle: Set[JFile] => Unit, delay: Time)
|
|
32 |
{
|
|
33 |
private val state = Synchronized(File_Watcher.State())
|
|
34 |
private val watcher = FileSystems.getDefault.newWatchService()
|
|
35 |
|
|
36 |
|
|
37 |
/* registered directories */
|
|
38 |
|
|
39 |
def register(dir: JFile): Unit =
|
|
40 |
state.change(st =>
|
|
41 |
st.dirs.get(dir) match {
|
|
42 |
case Some(key) if key.isValid => st
|
|
43 |
case _ =>
|
|
44 |
val key = dir.toPath.register(watcher, ENTRY_CREATE, ENTRY_DELETE, ENTRY_MODIFY)
|
|
45 |
st.copy(dirs = st.dirs + (dir -> key))
|
|
46 |
})
|
|
47 |
|
|
48 |
def deregister(dir: JFile): Unit =
|
|
49 |
state.change(st =>
|
|
50 |
st.dirs.get(dir) match {
|
|
51 |
case None => st
|
|
52 |
case Some(key) =>
|
|
53 |
key.cancel
|
|
54 |
st.copy(dirs = st.dirs - dir)
|
|
55 |
})
|
|
56 |
|
|
57 |
|
|
58 |
/* changed directory entries */
|
|
59 |
|
|
60 |
private val delay_changed = Standard_Thread.delay_last(delay)
|
|
61 |
{
|
|
62 |
val changed = state.change_result(st => (st.changed, st.copy(changed = Set.empty)))
|
|
63 |
handle(changed)
|
|
64 |
}
|
|
65 |
|
|
66 |
private val watcher_thread = Standard_Thread.fork("File_Watcher", daemon = true)
|
|
67 |
{
|
64700
|
68 |
try {
|
|
69 |
while (true) {
|
|
70 |
val key = watcher.take
|
|
71 |
val has_changed =
|
|
72 |
state.change_result(st =>
|
|
73 |
{
|
|
74 |
val (remove, changed) =
|
|
75 |
st.dirs.collectFirst({ case (dir, key1) if key == key1 => dir }) match {
|
|
76 |
case Some(dir) =>
|
|
77 |
val events =
|
|
78 |
JavaConversions.collectionAsScalaIterable(
|
|
79 |
key.pollEvents.asInstanceOf[java.util.List[WatchEvent[JPath]]])
|
|
80 |
val remove = if (key.reset) None else Some(dir)
|
|
81 |
val changed =
|
|
82 |
(Set.empty[JFile] /: events.iterator) {
|
|
83 |
case (set, event) => set + dir.toPath.resolve(event.context).toFile
|
|
84 |
}
|
|
85 |
(remove, changed)
|
|
86 |
case None =>
|
|
87 |
key.pollEvents
|
|
88 |
key.reset
|
|
89 |
(None, Set.empty[JFile])
|
|
90 |
}
|
|
91 |
(changed.nonEmpty, st.copy(dirs = st.dirs -- remove, changed = st.changed ++ changed))
|
|
92 |
})
|
|
93 |
if (has_changed) delay_changed.invoke()
|
|
94 |
}
|
64699
|
95 |
}
|
64700
|
96 |
catch { case Exn.Interrupt() => }
|
64699
|
97 |
}
|
|
98 |
|
|
99 |
|
|
100 |
/* shutdown */
|
|
101 |
|
64710
|
102 |
def shutdown()
|
64699
|
103 |
{
|
|
104 |
watcher_thread.interrupt
|
|
105 |
watcher_thread.join
|
|
106 |
delay_changed.revoke
|
|
107 |
}
|
|
108 |
}
|