# HG changeset patch
# User wenzelm
# Date 1483651702 -3600
# Node ID 7d556bb6046b26016b8bd029be7c25fc9a36b50b
# Parent  99f49258b02bb65d53418a3b770c1f0396f43bd8
dummy File_Watcher for Windows (spurious crashes seen on Windows 7);

diff -r 99f49258b02b -r 7d556bb6046b src/Pure/General/file_watcher.scala
--- a/src/Pure/General/file_watcher.scala	Thu Jan 05 21:34:04 2017 +0100
+++ b/src/Pure/General/file_watcher.scala	Thu Jan 05 22:28:22 2017 +0100
@@ -15,100 +15,109 @@
 import scala.collection.JavaConversions
 
 
+class File_Watcher private[File_Watcher]  // dummy template
+{
+  def register(dir: JFile) { }
+  def register_parent(file: JFile) { }
+  def deregister(dir: JFile) { }
+  def shutdown() { }
+}
+
 object File_Watcher
 {
   def apply(handle: Set[JFile] => Unit, delay: => Time = Time.seconds(0.5)): File_Watcher =
-    new File_Watcher(handle, delay)
+    if (Platform.is_windows) new File_Watcher
+    else new Impl(handle, delay)
 
 
-  /* internal state */
+  /* proper implementation */
 
   sealed case class State(
     dirs: Map[JFile, WatchKey] = Map.empty,
     changed: Set[JFile] = Set.empty)
-}
 
-class File_Watcher private(handle: Set[JFile] => Unit, delay: Time)
-{
-  private val state = Synchronized(File_Watcher.State())
-  private val watcher = FileSystems.getDefault.newWatchService()
+  class Impl private[File_Watcher](handle: Set[JFile] => Unit, delay: Time) extends File_Watcher
+  {
+    private val state = Synchronized(File_Watcher.State())
+    private val watcher = FileSystems.getDefault.newWatchService()
 
 
-  /* registered directories */
+    /* registered directories */
 
-  def register(dir: JFile): Unit =
-    state.change(st =>
-      st.dirs.get(dir) match {
-        case Some(key) if key.isValid => st
-        case _ =>
-          val key = dir.toPath.register(watcher, ENTRY_CREATE, ENTRY_DELETE, ENTRY_MODIFY)
-          st.copy(dirs = st.dirs + (dir -> key))
-      })
+    override def register(dir: JFile): Unit =
+      state.change(st =>
+        st.dirs.get(dir) match {
+          case Some(key) if key.isValid => st
+          case _ =>
+            val key = dir.toPath.register(watcher, ENTRY_CREATE, ENTRY_DELETE, ENTRY_MODIFY)
+            st.copy(dirs = st.dirs + (dir -> key))
+        })
 
-  def register_parent(file: JFile): Unit =
-  {
-    val dir = file.getParentFile
-    if (dir != null && dir.isDirectory) register(dir)
-  }
+    override def register_parent(file: JFile): Unit =
+    {
+      val dir = file.getParentFile
+      if (dir != null && dir.isDirectory) register(dir)
+    }
 
-  def deregister(dir: JFile): Unit =
-    state.change(st =>
-      st.dirs.get(dir) match {
-        case None => st
-        case Some(key) =>
-          key.cancel
-          st.copy(dirs = st.dirs - dir)
-      })
+    override def deregister(dir: JFile): Unit =
+      state.change(st =>
+        st.dirs.get(dir) match {
+          case None => st
+          case Some(key) =>
+            key.cancel
+            st.copy(dirs = st.dirs - dir)
+        })
 
 
-  /* changed directory entries */
+    /* changed directory entries */
 
-  private val delay_changed = Standard_Thread.delay_last(delay)
-  {
-    val changed = state.change_result(st => (st.changed, st.copy(changed = Set.empty)))
-    handle(changed)
-  }
+    private val delay_changed = Standard_Thread.delay_last(delay)
+    {
+      val changed = state.change_result(st => (st.changed, st.copy(changed = Set.empty)))
+      handle(changed)
+    }
 
-  private val watcher_thread = Standard_Thread.fork("File_Watcher", daemon = true)
-  {
-    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()
+    private val watcher_thread = Standard_Thread.fork("File_Watcher", daemon = true)
+    {
+      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() => }
     }
-    catch { case Exn.Interrupt() => }
-  }
 
 
-  /* shutdown */
+    /* shutdown */
 
-  def shutdown()
-  {
-    watcher_thread.interrupt
-    watcher_thread.join
-    delay_changed.revoke
+    override def shutdown()
+    {
+      watcher_thread.interrupt
+      watcher_thread.join
+      delay_changed.revoke
+    }
   }
 }