# HG changeset patch
# User wenzelm
# Date 1476533729 -7200
# Node ID 184e3a9327781b484415b76e27640c5eea502f9e
# Parent  407f69c4959f572cd84877e649d019f3eb742a9e
clarified signature;

diff -r 407f69c4959f -r 184e3a932778 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] =
     {