author | wenzelm |
Thu, 05 Jan 2017 22:28:22 +0100 | |
changeset 64807 | 7d556bb6046b |
parent 64782 | 3f0bbb60859b |
child 64858 | e31cf6eaecb8 |
permissions | -rw-r--r-- |
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 |
||
64807
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
18 |
class File_Watcher private[File_Watcher] // dummy template |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
19 |
{ |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
20 |
def register(dir: JFile) { } |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
21 |
def register_parent(file: JFile) { } |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
22 |
def deregister(dir: JFile) { } |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
23 |
def shutdown() { } |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
24 |
} |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
25 |
|
64699 | 26 |
object File_Watcher |
27 |
{ |
|
28 |
def apply(handle: Set[JFile] => Unit, delay: => Time = Time.seconds(0.5)): File_Watcher = |
|
64807
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
29 |
if (Platform.is_windows) new File_Watcher |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
30 |
else new Impl(handle, delay) |
64699 | 31 |
|
32 |
||
64807
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
33 |
/* proper implementation */ |
64699 | 34 |
|
35 |
sealed case class State( |
|
36 |
dirs: Map[JFile, WatchKey] = Map.empty, |
|
37 |
changed: Set[JFile] = Set.empty) |
|
38 |
||
64807
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
39 |
class Impl private[File_Watcher](handle: Set[JFile] => Unit, delay: Time) extends File_Watcher |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
40 |
{ |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
41 |
private val state = Synchronized(File_Watcher.State()) |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
42 |
private val watcher = FileSystems.getDefault.newWatchService() |
64699 | 43 |
|
44 |
||
64807
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
45 |
/* registered directories */ |
64699 | 46 |
|
64807
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
47 |
override def register(dir: JFile): Unit = |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
48 |
state.change(st => |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
49 |
st.dirs.get(dir) match { |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
50 |
case Some(key) if key.isValid => st |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
51 |
case _ => |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
52 |
val key = dir.toPath.register(watcher, ENTRY_CREATE, ENTRY_DELETE, ENTRY_MODIFY) |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
53 |
st.copy(dirs = st.dirs + (dir -> key)) |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
54 |
}) |
64699 | 55 |
|
64807
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
56 |
override def register_parent(file: JFile): Unit = |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
57 |
{ |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
58 |
val dir = file.getParentFile |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
59 |
if (dir != null && dir.isDirectory) register(dir) |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
60 |
} |
64782 | 61 |
|
64807
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
62 |
override def deregister(dir: JFile): Unit = |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
63 |
state.change(st => |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
64 |
st.dirs.get(dir) match { |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
65 |
case None => st |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
66 |
case Some(key) => |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
67 |
key.cancel |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
68 |
st.copy(dirs = st.dirs - dir) |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
69 |
}) |
64699 | 70 |
|
71 |
||
64807
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
72 |
/* changed directory entries */ |
64699 | 73 |
|
64807
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
74 |
private val delay_changed = Standard_Thread.delay_last(delay) |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
75 |
{ |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
76 |
val changed = state.change_result(st => (st.changed, st.copy(changed = Set.empty))) |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
77 |
handle(changed) |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
78 |
} |
64699 | 79 |
|
64807
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
80 |
private val watcher_thread = Standard_Thread.fork("File_Watcher", daemon = true) |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
81 |
{ |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
82 |
try { |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
83 |
while (true) { |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
84 |
val key = watcher.take |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
85 |
val has_changed = |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
86 |
state.change_result(st => |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
87 |
{ |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
88 |
val (remove, changed) = |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
89 |
st.dirs.collectFirst({ case (dir, key1) if key == key1 => dir }) match { |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
90 |
case Some(dir) => |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
91 |
val events = |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
92 |
JavaConversions.collectionAsScalaIterable( |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
93 |
key.pollEvents.asInstanceOf[java.util.List[WatchEvent[JPath]]]) |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
94 |
val remove = if (key.reset) None else Some(dir) |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
95 |
val changed = |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
96 |
(Set.empty[JFile] /: events.iterator) { |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
97 |
case (set, event) => set + dir.toPath.resolve(event.context).toFile |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
98 |
} |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
99 |
(remove, changed) |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
100 |
case None => |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
101 |
key.pollEvents |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
102 |
key.reset |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
103 |
(None, Set.empty[JFile]) |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
104 |
} |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
105 |
(changed.nonEmpty, st.copy(dirs = st.dirs -- remove, changed = st.changed ++ changed)) |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
106 |
}) |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
107 |
if (has_changed) delay_changed.invoke() |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
108 |
} |
64700 | 109 |
} |
64807
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
110 |
catch { case Exn.Interrupt() => } |
64699 | 111 |
} |
112 |
||
113 |
||
64807
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
114 |
/* shutdown */ |
64699 | 115 |
|
64807
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
116 |
override def shutdown() |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
117 |
{ |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
118 |
watcher_thread.interrupt |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
119 |
watcher_thread.join |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
120 |
delay_changed.revoke |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
121 |
} |
64699 | 122 |
} |
123 |
} |