src/Pure/General/file_watcher.scala
changeset 64700 14deaeaa6476
parent 64699 218c35908d5f
child 64710 72ca4e5f976e
equal deleted inserted replaced
64699:218c35908d5f 64700:14deaeaa6476
    63     handle(changed)
    63     handle(changed)
    64   }
    64   }
    65 
    65 
    66   private val watcher_thread = Standard_Thread.fork("File_Watcher", daemon = true)
    66   private val watcher_thread = Standard_Thread.fork("File_Watcher", daemon = true)
    67   {
    67   {
    68     while (true) {
    68     try {
    69       val key = watcher.take
    69       while (true) {
    70       val has_changed =
    70         val key = watcher.take
    71         state.change_result(st =>
    71         val has_changed =
    72           {
    72           state.change_result(st =>
    73             val (remove, changed) =
    73             {
    74               st.dirs.collectFirst({ case (dir, key1) if key == key1 => dir }) match {
    74               val (remove, changed) =
    75                 case Some(dir) =>
    75                 st.dirs.collectFirst({ case (dir, key1) if key == key1 => dir }) match {
    76                   val events =
    76                   case Some(dir) =>
    77                     JavaConversions.collectionAsScalaIterable(
    77                     val events =
    78                       key.pollEvents.asInstanceOf[java.util.List[WatchEvent[JPath]]])
    78                       JavaConversions.collectionAsScalaIterable(
    79                   val remove = if (key.reset) None else Some(dir)
    79                         key.pollEvents.asInstanceOf[java.util.List[WatchEvent[JPath]]])
    80                   val changed =
    80                     val remove = if (key.reset) None else Some(dir)
    81                     (Set.empty[JFile] /: events.iterator) {
    81                     val changed =
    82                       case (set, event) => set + dir.toPath.resolve(event.context).toFile
    82                       (Set.empty[JFile] /: events.iterator) {
    83                     }
    83                         case (set, event) => set + dir.toPath.resolve(event.context).toFile
    84                   (remove, changed)
    84                       }
    85                 case None =>
    85                     (remove, changed)
    86                   key.pollEvents
    86                   case None =>
    87                   key.reset
    87                     key.pollEvents
    88                   (None, Set.empty[JFile])
    88                     key.reset
    89               }
    89                     (None, Set.empty[JFile])
    90             (changed.nonEmpty, st.copy(dirs = st.dirs -- remove, changed = st.changed ++ changed))
    90                 }
    91           })
    91               (changed.nonEmpty, st.copy(dirs = st.dirs -- remove, changed = st.changed ++ changed))
    92       if (has_changed) delay_changed.invoke()
    92             })
       
    93         if (has_changed) delay_changed.invoke()
       
    94       }
    93     }
    95     }
       
    96     catch { case Exn.Interrupt() => }
    94   }
    97   }
    95 
    98 
    96 
    99 
    97   /* shutdown */
   100   /* shutdown */
    98 
   101