clarified signature;
authorwenzelm
Sat, 15 Oct 2016 14:15:29 +0200
changeset 64222 184e3a932778
parent 64221 407f69c4959f
child 64223 9d5b9f41df77
clarified signature;
src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Sat Oct 15 13:07:54 2016 +0200
+++ b/src/Pure/General/ssh.scala	Sat Oct 15 14:15:29 2016 +0200
@@ -11,7 +11,7 @@
 
 import scala.collection.{mutable, JavaConversions}
 
-import com.jcraft.jsch.{JSch, Logger => JSch_Logger, Session => JSch_Session,
+import com.jcraft.jsch.{JSch, Logger => JSch_Logger, Session => JSch_Session, SftpException,
   OpenSSHConfig, UserInfo, Channel => JSch_Channel, ChannelExec, ChannelSftp, SftpATTRS}
 
 
@@ -138,8 +138,12 @@
     def mkdir(remote_path: String) { channel.mkdir(remote_path) }
     def rmdir(remote_path: String) { channel.rmdir(remote_path) }
 
-    def stat(remote_path: String): Dir_Entry =
-      Dir_Entry(remote_path, channel.stat(remote_path))
+    def stat(remote_path: String): Option[Dir_Entry] =
+      try { Some(Dir_Entry(remote_path, channel.stat(remote_path))) }
+      catch { case _: SftpException => None }
+
+    def is_file(remote_path: String): Boolean = stat(remote_path).map(_.is_file) getOrElse false
+    def is_dir(remote_path: String): Boolean = stat(remote_path).map(_.is_dir) getOrElse false
 
     def read_dir(remote_path: String): List[Dir_Entry] =
     {