# HG changeset patch
# User wenzelm
# Date 1485087098 -3600
# Node ID 89c0896a19adc9a7743fdd1093be9c0cd58173cc
# Parent  111d58654822acb7845916e8f78a6612b32de623
clarified operation: include dirs as well;

diff -r 111d58654822 -r 89c0896a19ad src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Sun Jan 22 12:57:52 2017 +0100
+++ b/src/Pure/General/file.scala	Sun Jan 22 13:11:38 2017 +0100
@@ -122,18 +122,26 @@
     else files.toList.map(_.getName)
   }
 
-  def find_files(start: JFile, pred: JFile => Boolean = _ => true): List[JFile] =
+  def find_files(
+    start: JFile,
+    pred: JFile => Boolean = _ => true,
+    include_dirs: Boolean = false): List[JFile] =
   {
     val result = new mutable.ListBuffer[JFile]
+    def check(file: JFile) { if (pred(file)) result += file }
 
-    if (start.isFile && pred(start)) result += start
+    if (start.isFile) check(start)
     else if (start.isDirectory) {
       Files.walkFileTree(start.toPath,
         new SimpleFileVisitor[JPath] {
+          override def preVisitDirectory(path: JPath, attrs: BasicFileAttributes): FileVisitResult =
+          {
+            if (include_dirs) check(path.toFile)
+            FileVisitResult.CONTINUE
+          }
           override def visitFile(path: JPath, attrs: BasicFileAttributes): FileVisitResult =
           {
-            val file = path.toFile
-            if (pred(file)) result += file
+            check(path.toFile)
             FileVisitResult.CONTINUE
           }
         }