# HG changeset patch
# User wenzelm
# Date 1456666433 -3600
# Node ID 133f65ac17e590960ca42c8f329b0c6f45eea90d
# Parent  26e4be6a680f5f285119e5fecd6c9439ab4d69f7
just one File.find_files, based on Java 7 Files operations;

diff -r 26e4be6a680f -r 133f65ac17e5 src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Sun Feb 28 12:05:52 2016 +0100
+++ b/src/Pure/General/file.scala	Sun Feb 28 14:33:53 2016 +0100
@@ -10,7 +10,8 @@
 import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream,
   OutputStream, InputStream, FileInputStream, BufferedInputStream, BufferedReader,
   InputStreamReader, File => JFile, IOException}
-import java.nio.file.{StandardCopyOption, Files}
+import java.nio.file.{StandardCopyOption, Path => JPath, Files, SimpleFileVisitor, FileVisitResult}
+import java.nio.file.attribute.BasicFileAttributes
 import java.net.{URL, URLDecoder, MalformedURLException}
 import java.util.zip.{GZIPInputStream, GZIPOutputStream}
 import java.util.regex.Pattern
@@ -107,24 +108,29 @@
   def shell_path(file: JFile): String = shell_quote(standard_path(file))
 
 
-  /* directory content */
+  /* find files */
 
-  def read_dir(dir: Path): List[String] =
+  def find_files(start: JFile, pred: JFile => Boolean = _ => true): List[JFile] =
   {
-    if (!dir.is_dir) error("Bad directory: " + dir.toString)
-    val files = dir.file.listFiles
-    if (files == null) Nil
-    else files.toList.map(_.getName)
+    val result = new mutable.ListBuffer[JFile]
+
+    if (start.isFile && pred(start)) result += start
+    else if (start.isDirectory) {
+      Files.walkFileTree(start.toPath,
+        new SimpleFileVisitor[JPath] {
+          override def visitFile(path: JPath, attrs: BasicFileAttributes): FileVisitResult =
+          {
+            val file = path.toFile
+            if (pred(file)) result += file
+            FileVisitResult.CONTINUE
+          }
+        }
+      )
+    }
+
+    result.toList
   }
 
-  def find_files(dir: Path): Stream[Path] =
-    read_dir(dir).toStream.map(name =>
-      if (Path.is_wellformed(name)) {
-        val path = dir + Path.basic(name)
-        path #:: (if (path.is_dir) find_files(path) else Stream.empty)
-      }
-      else Stream.empty).flatten
-
 
   /* read */
 
diff -r 26e4be6a680f -r 133f65ac17e5 src/Tools/jEdit/src/scala_console.scala
--- a/src/Tools/jEdit/src/scala_console.scala	Sun Feb 28 12:05:52 2016 +0100
+++ b/src/Tools/jEdit/src/scala_console.scala	Sun Feb 28 14:33:53 2016 +0100
@@ -27,23 +27,10 @@
 
   private def reconstruct_classpath(): String =
   {
-    def find_files(start: JFile, ok: JFile => Boolean = _ => true): List[JFile] =
-    {
-      val files = new mutable.ListBuffer[JFile]
-      val filter = new FileFilter { def accept(entry: JFile) = entry.isDirectory || ok(entry) }
-      def find_entry(entry: JFile)
-      {
-        if (ok(entry)) files += entry
-        if (entry.isDirectory) entry.listFiles(filter).foreach(find_entry)
-      }
-      find_entry(start)
-      files.toList
-    }
-
     def find_jars(start: String): List[String] =
       if (start != null)
-        find_files(new JFile(start),
-          entry => entry.isFile && entry.getName.endsWith(".jar")).map(_.getAbsolutePath)
+        File.find_files(new JFile(start), file => file.getName.endsWith(".jar")).
+          map(_.getAbsolutePath)
       else Nil
 
     val initial_class_path =