equal
deleted
inserted
replaced
18 class File_Watcher private[File_Watcher] // dummy template |
18 class File_Watcher private[File_Watcher] // dummy template |
19 { |
19 { |
20 def register(dir: JFile) { } |
20 def register(dir: JFile) { } |
21 def register_parent(file: JFile) { } |
21 def register_parent(file: JFile) { } |
22 def deregister(dir: JFile) { } |
22 def deregister(dir: JFile) { } |
|
23 def purge(retain: Set[JFile]) { } |
23 def shutdown() { } |
24 def shutdown() { } |
24 } |
25 } |
25 |
26 |
26 object File_Watcher |
27 object File_Watcher |
27 { |
28 { |
73 case Some(key) => |
74 case Some(key) => |
74 key.cancel |
75 key.cancel |
75 st.copy(dirs = st.dirs - dir) |
76 st.copy(dirs = st.dirs - dir) |
76 }) |
77 }) |
77 |
78 |
|
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 |
78 |
84 |
79 /* changed directory entries */ |
85 /* changed directory entries */ |
80 |
86 |
81 private val delay_changed = Standard_Thread.delay_last(delay) |
87 private val delay_changed = Standard_Thread.delay_last(delay) |
82 { |
88 { |