# HG changeset patch
# User wenzelm
# Date 1484000830 -3600
# Node ID e600cfdc9e9746a571f10a77824ab92f84e95ba0
# Parent  e31cf6eaecb8548b354f12dc4da80966137f0276
tuned output;

diff -r e31cf6eaecb8 -r e600cfdc9e97 src/Pure/General/file_watcher.scala
--- a/src/Pure/General/file_watcher.scala	Mon Jan 09 22:54:48 2017 +0100
+++ b/src/Pure/General/file_watcher.scala	Mon Jan 09 23:27:10 2017 +0100
@@ -26,6 +26,9 @@
 object File_Watcher
 {
   val none: File_Watcher = new File_Watcher
+  {
+    override def toString: String = "File_Watcher.none"
+  }
 
   def apply(handle: Set[JFile] => Unit, delay: => Time = Time.seconds(0.5)): File_Watcher =
     if (Platform.is_windows) none else new Impl(handle, delay)
@@ -42,6 +45,9 @@
     private val state = Synchronized(File_Watcher.State())
     private val watcher = FileSystems.getDefault.newWatchService()
 
+    override def toString: String =
+      state.value.dirs.keySet.mkString("File_Watcher(", ", ", ")")
+
 
     /* registered directories */