diff -r 218c35908d5f -r 14deaeaa6476 src/Pure/General/file_watcher.scala
--- a/src/Pure/General/file_watcher.scala	Thu Dec 29 15:32:13 2016 +0100
+++ b/src/Pure/General/file_watcher.scala	Thu Dec 29 15:37:15 2016 +0100
@@ -65,32 +65,35 @@
 
   private val watcher_thread = Standard_Thread.fork("File_Watcher", daemon = true)
   {
-    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()
+    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() => }
   }