author | wenzelm |
Fri, 19 Jun 2020 18:22:03 +0200 | |
changeset 71961 | af779738a8f9 |
parent 71704 | b9a5eb0f3b43 |
child 73340 | 0ffcad1f6130 |
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 |
||
71359
411c0322c09d
eliminated deprecated scala.collection.JavaConversions;
wenzelm
parents:
64867
diff
changeset
|
15 |
import scala.collection.JavaConverters |
64699 | 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) { } |
64867 | 23 |
def purge(retain: Set[JFile]) { } |
64807
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
24 |
def shutdown() { } |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
25 |
} |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
26 |
|
64699 | 27 |
object File_Watcher |
28 |
{ |
|
64858 | 29 |
val none: File_Watcher = new File_Watcher |
64859 | 30 |
{ |
31 |
override def toString: String = "File_Watcher.none" |
|
32 |
} |
|
64858 | 33 |
|
64699 | 34 |
def apply(handle: Set[JFile] => Unit, delay: => Time = Time.seconds(0.5)): File_Watcher = |
64858 | 35 |
if (Platform.is_windows) none else new Impl(handle, delay) |
64699 | 36 |
|
37 |
||
64807
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
38 |
/* proper implementation */ |
64699 | 39 |
|
40 |
sealed case class State( |
|
41 |
dirs: Map[JFile, WatchKey] = Map.empty, |
|
42 |
changed: Set[JFile] = Set.empty) |
|
43 |
||
64807
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
44 |
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
|
45 |
{ |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
46 |
private val state = Synchronized(File_Watcher.State()) |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
47 |
private val watcher = FileSystems.getDefault.newWatchService() |
64699 | 48 |
|
64859 | 49 |
override def toString: String = |
50 |
state.value.dirs.keySet.mkString("File_Watcher(", ", ", ")") |
|
51 |
||
64699 | 52 |
|
64807
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
53 |
/* registered directories */ |
64699 | 54 |
|
64807
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
55 |
override def register(dir: JFile): Unit = |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
56 |
state.change(st => |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
57 |
st.dirs.get(dir) match { |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
58 |
case Some(key) if key.isValid => st |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
59 |
case _ => |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
60 |
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
|
61 |
st.copy(dirs = st.dirs + (dir -> key)) |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
62 |
}) |
64699 | 63 |
|
64807
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
64 |
override def register_parent(file: JFile): Unit = |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
65 |
{ |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
66 |
val dir = file.getParentFile |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
67 |
if (dir != null && dir.isDirectory) register(dir) |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
68 |
} |
64782 | 69 |
|
64807
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
70 |
override def deregister(dir: JFile): Unit = |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
71 |
state.change(st => |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
72 |
st.dirs.get(dir) match { |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
73 |
case None => st |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
74 |
case Some(key) => |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
75 |
key.cancel |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
76 |
st.copy(dirs = st.dirs - dir) |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
77 |
}) |
64699 | 78 |
|
64867 | 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 |
||
64699 | 84 |
|
64807
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
85 |
/* changed directory entries */ |
64699 | 86 |
|
71704 | 87 |
private val delay_changed = Delay.last(delay) |
64807
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 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
|
90 |
handle(changed) |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
91 |
} |
64699 | 92 |
|
71692 | 93 |
private val watcher_thread = Isabelle_Thread.fork(name = "file_watcher", daemon = true) |
64807
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
94 |
{ |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
95 |
try { |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
96 |
while (true) { |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
97 |
val key = watcher.take |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
98 |
val has_changed = |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
99 |
state.change_result(st => |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
100 |
{ |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
101 |
val (remove, changed) = |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
102 |
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
|
103 |
case Some(dir) => |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
104 |
val events = |
71359
411c0322c09d
eliminated deprecated scala.collection.JavaConversions;
wenzelm
parents:
64867
diff
changeset
|
105 |
JavaConverters.collectionAsScalaIterable( |
64807
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
106 |
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
|
107 |
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
|
108 |
val changed = |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
109 |
(Set.empty[JFile] /: events.iterator) { |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
110 |
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
|
111 |
} |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
112 |
(remove, changed) |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
113 |
case None => |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
114 |
key.pollEvents |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
115 |
key.reset |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
116 |
(None, Set.empty[JFile]) |
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 |
(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
|
119 |
}) |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
120 |
if (has_changed) delay_changed.invoke() |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
121 |
} |
64700 | 122 |
} |
64807
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
123 |
catch { case Exn.Interrupt() => } |
64699 | 124 |
} |
125 |
||
126 |
||
64807
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
127 |
/* shutdown */ |
64699 | 128 |
|
64807
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
129 |
override def shutdown() |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
130 |
{ |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
131 |
watcher_thread.interrupt |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
132 |
watcher_thread.join |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
133 |
delay_changed.revoke |
7d556bb6046b
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);
wenzelm
parents:
64782
diff
changeset
|
134 |
} |
64699 | 135 |
} |
136 |
} |