diff -r 316d703f741d -r e31cf6eaecb8 src/Pure/General/file_watcher.scala
--- a/src/Pure/General/file_watcher.scala	Mon Jan 09 21:51:39 2017 +0100
+++ b/src/Pure/General/file_watcher.scala	Mon Jan 09 22:54:48 2017 +0100
@@ -25,9 +25,10 @@
 
 object File_Watcher
 {
+  val none: File_Watcher = new File_Watcher
+
   def apply(handle: Set[JFile] => Unit, delay: => Time = Time.seconds(0.5)): File_Watcher =
-    if (Platform.is_windows) new File_Watcher
-    else new Impl(handle, delay)
+    if (Platform.is_windows) none else new Impl(handle, delay)
 
 
   /* proper implementation */