1/* Title: Pure/General/file_watcher.scala 2 Author: Makarius 3 4Watcher for file-system events. 5*/ 6 7package isabelle 8 9 10import java.io.{File => JFile} 11import java.nio.file.FileSystems 12import java.nio.file.{WatchKey, WatchEvent, Path => JPath} 13import java.nio.file.StandardWatchEventKinds.{ENTRY_CREATE, ENTRY_DELETE, ENTRY_MODIFY} 14 15import scala.collection.JavaConverters 16 17 18class File_Watcher private[File_Watcher] // dummy template 19{ 20 def register(dir: JFile) { } 21 def register_parent(file: JFile) { } 22 def deregister(dir: JFile) { } 23 def purge(retain: Set[JFile]) { } 24 def shutdown() { } 25} 26 27object File_Watcher 28{ 29 val none: File_Watcher = new File_Watcher 30 { 31 override def toString: String = "File_Watcher.none" 32 } 33 34 def apply(handle: Set[JFile] => Unit, delay: => Time = Time.seconds(0.5)): File_Watcher = 35 if (Platform.is_windows) none else new Impl(handle, delay) 36 37 38 /* proper implementation */ 39 40 sealed case class State( 41 dirs: Map[JFile, WatchKey] = Map.empty, 42 changed: Set[JFile] = Set.empty) 43 44 class Impl private[File_Watcher](handle: Set[JFile] => Unit, delay: Time) extends File_Watcher 45 { 46 private val state = Synchronized(File_Watcher.State()) 47 private val watcher = FileSystems.getDefault.newWatchService() 48 49 override def toString: String = 50 state.value.dirs.keySet.mkString("File_Watcher(", ", ", ")") 51 52 53 /* registered directories */ 54 55 override def register(dir: JFile): Unit = 56 state.change(st => 57 st.dirs.get(dir) match { 58 case Some(key) if key.isValid => st 59 case _ => 60 val key = dir.toPath.register(watcher, ENTRY_CREATE, ENTRY_DELETE, ENTRY_MODIFY) 61 st.copy(dirs = st.dirs + (dir -> key)) 62 }) 63 64 override def register_parent(file: JFile): Unit = 65 { 66 val dir = file.getParentFile 67 if (dir != null && dir.isDirectory) register(dir) 68 } 69 70 override def deregister(dir: JFile): Unit = 71 state.change(st => 72 st.dirs.get(dir) match { 73 case None => st 74 case Some(key) => 75 key.cancel 76 st.copy(dirs = st.dirs - dir) 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 84 85 /* changed directory entries */ 86 87 private val delay_changed = Standard_Thread.delay_last(delay) 88 { 89 val changed = state.change_result(st => (st.changed, st.copy(changed = Set.empty))) 90 handle(changed) 91 } 92 93 private val watcher_thread = Standard_Thread.fork("File_Watcher", daemon = true) 94 { 95 try { 96 while (true) { 97 val key = watcher.take 98 val has_changed = 99 state.change_result(st => 100 { 101 val (remove, changed) = 102 st.dirs.collectFirst({ case (dir, key1) if key == key1 => dir }) match { 103 case Some(dir) => 104 val events = 105 JavaConverters.collectionAsScalaIterable( 106 key.pollEvents.asInstanceOf[java.util.List[WatchEvent[JPath]]]) 107 val remove = if (key.reset) None else Some(dir) 108 val changed = 109 (Set.empty[JFile] /: events.iterator) { 110 case (set, event) => set + dir.toPath.resolve(event.context).toFile 111 } 112 (remove, changed) 113 case None => 114 key.pollEvents 115 key.reset 116 (None, Set.empty[JFile]) 117 } 118 (changed.nonEmpty, st.copy(dirs = st.dirs -- remove, changed = st.changed ++ changed)) 119 }) 120 if (has_changed) delay_changed.invoke() 121 } 122 } 123 catch { case Exn.Interrupt() => } 124 } 125 126 127 /* shutdown */ 128 129 override def shutdown() 130 { 131 watcher_thread.interrupt 132 watcher_thread.join 133 delay_changed.revoke 134 } 135 } 136} 137