src/Pure/General/file_watcher.scala
changeset 73359 d8a0e996614b
parent 73353 279e45248e9d
child 73367 77ef8bef0593
equal deleted inserted replaced
73358:78aa7846e91f 73359:d8a0e996614b
   103                     case Some(dir) =>
   103                     case Some(dir) =>
   104                       val events: Iterable[WatchEvent[JPath]] =
   104                       val events: Iterable[WatchEvent[JPath]] =
   105                         key.pollEvents.asInstanceOf[java.util.List[WatchEvent[JPath]]].asScala
   105                         key.pollEvents.asInstanceOf[java.util.List[WatchEvent[JPath]]].asScala
   106                       val remove = if (key.reset) None else Some(dir)
   106                       val remove = if (key.reset) None else Some(dir)
   107                       val changed =
   107                       val changed =
   108                         (Set.empty[JFile] /: events.iterator) {
   108                         events.iterator.foldLeft(Set.empty[JFile]) {
   109                           case (set, event) => set + dir.toPath.resolve(event.context).toFile
   109                           case (set, event) => set + dir.toPath.resolve(event.context).toFile
   110                         }
   110                         }
   111                       (remove, changed)
   111                       (remove, changed)
   112                     case None =>
   112                     case None =>
   113                       key.pollEvents
   113                       key.pollEvents