src/Pure/General/ssh.scala
changeset 69301 f6c17b9e1104
parent 69300 8b6ab9989bcd
child 69302 5faf57207a9b
--- a/src/Pure/General/ssh.scala	Wed Nov 14 16:26:58 2018 +0100
+++ b/src/Pure/General/ssh.scala	Wed Nov 14 20:04:39 2018 +0100
@@ -356,6 +356,10 @@
       }
     }
 
+    def is_link(path: Path): Boolean =
+      try { sftp.lstat(remote_path(path)).isLink }
+      catch { case _: SftpException => false }
+
     override def is_dir(path: Path): Boolean = check_entry(path, true)
     override def is_file(path: Path): Boolean = check_entry(path, false)
 
@@ -381,17 +385,29 @@
       } yield Dir_Entry(Path.basic(name), test_dir(dir_name + "/" + name, attrs))).toList
     }
 
-    def find_files(root: Path, pred: Dir_Entry => Boolean = _ => true): List[Dir_Entry] =
+    def find_files(
+      start: Path,
+      pred: Path => Boolean = _ => true,
+      include_dirs: Boolean = false,
+      follow_links: Boolean = false): List[Path] =
     {
-      def find(dir: Path): List[Dir_Entry] =
-        read_dir(dir).flatMap(entry =>
-          {
-            val file = dir + entry.name
-            if (entry.is_dir) find(file)
-            else if (pred(entry)) List(entry.copy(name = file))
-            else Nil
-          })
-      find(root)
+      val result = new mutable.ListBuffer[Path]
+      def check(path: Path) { if (pred(path)) result += path }
+
+      def find(dir: Path)
+      {
+        if (follow_links || !is_link(dir)) {
+          if (include_dirs) check(dir)
+          for (entry <- read_dir(dir)) {
+            val path = dir + entry.name
+            if (include_dirs || entry.is_file) check(path)
+            if (entry.is_dir) find(path)
+          }
+        }
+      }
+      if (is_file(start)) check(start) else find(start)
+
+      result.toList
     }
 
     def open_input(path: Path): InputStream = sftp.get(remote_path(path))