# HG changeset patch
# User wenzelm
# Date 1542209218 -3600
# Node ID 8b6ab9989bcdecaaf8d50e7e13e2d7c48c32b3b7
# Parent  2fd070377c997408434d8debb22476a087dc3617
is_file/is_dir/read_dir: more uniform treatment of errors and boundary cases, notably for symlinks in ssh;

diff -r 2fd070377c99 -r 8b6ab9989bcd src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Wed Nov 14 11:51:03 2018 +0100
+++ b/src/Pure/General/file.ML	Wed Nov 14 16:26:58 2018 +0100
@@ -15,6 +15,7 @@
   val exists: Path.T -> bool
   val rm: Path.T -> unit
   val is_dir: Path.T -> bool
+  val is_file: Path.T -> bool
   val check_dir: Path.T -> Path.T
   val check_file: Path.T -> Path.T
   val open_dir: (OS.FileSys.dirstream -> 'a) -> Path.T -> 'a
@@ -74,15 +75,16 @@
 
 val rm = OS.FileSys.remove o platform_path;
 
-fun is_dir path =
-  the_default false (try OS.FileSys.isDir (platform_path path));
+fun test_dir path = the_default false (try OS.FileSys.isDir (platform_path path));
+fun is_dir path = exists path andalso test_dir path;
+fun is_file path = exists path andalso not (test_dir path);
 
 fun check_dir path =
-  if exists path andalso is_dir path then path
+  if is_dir path then path
   else error ("No such directory: " ^ Path.print (Path.expand path));
 
 fun check_file path =
-  if exists path andalso not (is_dir path) then path
+  if is_file path then path
   else error ("No such file: " ^ Path.print (Path.expand path));
 
 
@@ -106,13 +108,14 @@
 
 (* directory content *)
 
-fun fold_dir f path a = open_dir (fn stream =>
-  let
-    fun read x =
-      (case OS.FileSys.readDir stream of
-        NONE => x
-      | SOME entry => read (f entry x));
-  in read a end) path;
+fun fold_dir f path a =
+  check_dir path |> open_dir (fn stream =>
+    let
+      fun read x =
+        (case OS.FileSys.readDir stream of
+          NONE => x
+        | SOME entry => read (f entry x));
+    in read a end);
 
 fun read_dir path = rev (fold_dir cons path []);
 
diff -r 2fd070377c99 -r 8b6ab9989bcd src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Wed Nov 14 11:51:03 2018 +0100
+++ b/src/Pure/General/file.scala	Wed Nov 14 16:26:58 2018 +0100
@@ -141,7 +141,7 @@
 
   def read_dir(dir: Path): List[String] =
   {
-    if (!dir.is_dir) error("Bad directory: " + dir.toString)
+    if (!dir.is_dir) error("No such directory: " + dir.toString)
     val files = dir.file.listFiles
     if (files == null) Nil
     else files.toList.map(_.getName)
diff -r 2fd070377c99 -r 8b6ab9989bcd src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Wed Nov 14 11:51:03 2018 +0100
+++ b/src/Pure/General/ssh.scala	Wed Nov 14 16:26:58 2018 +0100
@@ -201,10 +201,9 @@
 
   type Attrs = SftpATTRS
 
-  sealed case class Dir_Entry(name: Path, attrs: Attrs)
+  sealed case class Dir_Entry(name: Path, is_dir: Boolean)
   {
-    def is_file: Boolean = attrs.isReg
-    def is_dir: Boolean = attrs.isDir
+    def is_file: Boolean = !is_dir
   }
 
 
@@ -341,12 +340,24 @@
     def mkdir(path: Path): Unit = sftp.mkdir(remote_path(path))
     def rmdir(path: Path): Unit = sftp.rmdir(remote_path(path))
 
-    def stat(path: Path): Option[Dir_Entry] =
-      try { Some(Dir_Entry(expand_path(path), sftp.stat(remote_path(path)))) }
+    private def try_stat(name: String): Option[Attrs] =
+      try { Some(sftp.stat(name)) }
       catch { case _: SftpException => None }
 
-    override def is_file(path: Path): Boolean = stat(path).map(_.is_file) getOrElse false
-    override def is_dir(path: Path): Boolean = stat(path).map(_.is_dir) getOrElse false
+    private def test_dir(name: String, attrs: Attrs): Boolean =
+      if (attrs.isLink) try_stat(name + "/.").isDefined else attrs.isDir
+
+    private def check_entry(path: Path, as_dir: Boolean): Boolean =
+    {
+      val name = remote_path(path)
+      try_stat(name) match {
+        case None => false
+        case Some(attrs) => if (as_dir) test_dir(name, attrs) else !test_dir(name, attrs)
+      }
+    }
+
+    override def is_dir(path: Path): Boolean = check_entry(path, true)
+    override def is_file(path: Path): Boolean = check_entry(path, false)
 
     override def mkdirs(path: Path): Unit =
       if (!is_dir(path)) {
@@ -357,14 +368,17 @@
 
     def read_dir(path: Path): List[Dir_Entry] =
     {
-      val dir = sftp.ls(remote_path(path))
+      if (!is_dir(path)) error("No such directory: " + path.toString)
+
+      val dir_name = remote_path(path)
+      val dir = sftp.ls(dir_name)
       (for {
         i <- (0 until dir.size).iterator
         a = dir.get(i).asInstanceOf[AnyRef]
         name = Untyped.get[String](a, "filename")
         attrs = Untyped.get[Attrs](a, "attrs")
         if name != "." && name != ".."
-      } yield Dir_Entry(Path.basic(name), attrs)).toList
+      } 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] =
@@ -440,8 +454,8 @@
 
     def expand_path(path: Path): Path = path.expand
     def bash_path(path: Path): String = File.bash_path(path)
+    def is_dir(path: Path): Boolean = path.is_dir
     def is_file(path: Path): Boolean = path.is_file
-    def is_dir(path: Path): Boolean = path.is_dir
     def mkdirs(path: Path): Unit = Isabelle_System.mkdirs(path)
 
     def execute(command: String,