--- a/src/Pure/General/file_watcher.scala Thu Dec 29 15:32:13 2016 +0100
+++ b/src/Pure/General/file_watcher.scala Thu Dec 29 15:37:15 2016 +0100
@@ -65,32 +65,35 @@
private val watcher_thread = Standard_Thread.fork("File_Watcher", daemon = true)
{
- while (true) {
- val key = watcher.take
- val has_changed =
- state.change_result(st =>
- {
- val (remove, changed) =
- st.dirs.collectFirst({ case (dir, key1) if key == key1 => dir }) match {
- case Some(dir) =>
- val events =
- JavaConversions.collectionAsScalaIterable(
- key.pollEvents.asInstanceOf[java.util.List[WatchEvent[JPath]]])
- val remove = if (key.reset) None else Some(dir)
- val changed =
- (Set.empty[JFile] /: events.iterator) {
- case (set, event) => set + dir.toPath.resolve(event.context).toFile
- }
- (remove, changed)
- case None =>
- key.pollEvents
- key.reset
- (None, Set.empty[JFile])
- }
- (changed.nonEmpty, st.copy(dirs = st.dirs -- remove, changed = st.changed ++ changed))
- })
- if (has_changed) delay_changed.invoke()
+ try {
+ while (true) {
+ val key = watcher.take
+ val has_changed =
+ state.change_result(st =>
+ {
+ val (remove, changed) =
+ st.dirs.collectFirst({ case (dir, key1) if key == key1 => dir }) match {
+ case Some(dir) =>
+ val events =
+ JavaConversions.collectionAsScalaIterable(
+ key.pollEvents.asInstanceOf[java.util.List[WatchEvent[JPath]]])
+ val remove = if (key.reset) None else Some(dir)
+ val changed =
+ (Set.empty[JFile] /: events.iterator) {
+ case (set, event) => set + dir.toPath.resolve(event.context).toFile
+ }
+ (remove, changed)
+ case None =>
+ key.pollEvents
+ key.reset
+ (None, Set.empty[JFile])
+ }
+ (changed.nonEmpty, st.copy(dirs = st.dirs -- remove, changed = st.changed ++ changed))
+ })
+ if (has_changed) delay_changed.invoke()
+ }
}
+ catch { case Exn.Interrupt() => }
}