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