--- 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 */