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