src/Pure/General/file.scala

 
 import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream,
   OutputStream, InputStream, FileInputStream, BufferedInputStream, BufferedReader,
   InputStreamReader, File => JFile, IOException}
 import java.nio.file.{StandardOpenOption, StandardCopyOption, Path => JPath,
-  Files, SimpleFileVisitor, FileVisitResult}
+  Files, SimpleFileVisitor, FileVisitOption, FileVisitResult}
 import java.nio.file.attribute.BasicFileAttributes
 import java.net.{URL, MalformedURLException}
 import java.util.zip.{GZIPInputStream, GZIPOutputStream}
 import java.util.regex.Pattern
+import java.util.EnumSet
 
 import org.tukaani.xz.{XZInputStream, XZOutputStream}
 
 import scala.collection.mutable
 import scala.util.matching.Regex

   }
 
   def find_files(
     start: JFile,
     pred: JFile => Boolean = _ => true,
-    include_dirs: Boolean = false): List[JFile] =
+    include_dirs: Boolean = false,
+    follow_links: Boolean = true): List[JFile] =
   {
     val result = new mutable.ListBuffer[JFile]
     def check(file: JFile) { if (pred(file)) result += file }
 
     if (start.isFile) check(start)
     else if (start.isDirectory) {
-      Files.walkFileTree(start.toPath,
+      val options =
+        if (follow_links) EnumSet.of(FileVisitOption.FOLLOW_LINKS)
+        else EnumSet.noneOf(classOf[FileVisitOption])
+      Files.walkFileTree(start.toPath, options, Integer.MAX_VALUE,
         new SimpleFileVisitor[JPath] {
           override def preVisitDirectory(path: JPath, attrs: BasicFileAttributes): FileVisitResult =
           {
             if (include_dirs) check(path.toFile)
             FileVisitResult.CONTINUE