src/Pure/General/ssh.scala
changeset 64233 ef6f7e8a018c
parent 64228 b46969a851a9
child 64254 b1aef25ce8df
equal deleted inserted replaced
64232:367d83d6030e 64233:ef6f7e8a018c
   116 
   116 
   117   /* Sftp channel */
   117   /* Sftp channel */
   118 
   118 
   119   type Attrs = SftpATTRS
   119   type Attrs = SftpATTRS
   120 
   120 
   121   sealed case class Dir_Entry(name: String, attrs: Attrs)
   121   sealed case class Dir_Entry(name: Path, attrs: Attrs)
   122   {
   122   {
   123     def is_file: Boolean = attrs.isReg
   123     def is_file: Boolean = attrs.isReg
   124     def is_dir: Boolean = attrs.isDir
   124     def is_dir: Boolean = attrs.isDir
   125   }
   125   }
   126 
   126 
   132     val settings: Map[String, String] =
   132     val settings: Map[String, String] =
   133     {
   133     {
   134       val home = channel.getHome
   134       val home = channel.getHome
   135       Map("HOME" -> home, "USER_HOME" -> home)
   135       Map("HOME" -> home, "USER_HOME" -> home)
   136     }
   136     }
   137     def path(p: Path): String = p.expand_env(settings).implode
   137     def expand_path(path: Path): Path = path.expand_env(settings)
   138 
   138     def remote_path(path: Path): String = expand_path(path).implode
   139     def chmod(permissions: Int, remote_path: String) { channel.chmod(permissions, remote_path) }
   139 
   140     def mv(remote_path1: String, remote_path2: String): Unit =
   140     def chmod(permissions: Int, path: Path): Unit = channel.chmod(permissions, remote_path(path))
   141       channel.rename(remote_path1, remote_path2)
   141     def mv(path1: Path, path2: Path): Unit = channel.rename(remote_path(path1), remote_path(path2))
   142     def rm(remote_path: String) { channel.rm(remote_path) }
   142     def rm(path: Path): Unit = channel.rm(remote_path(path))
   143     def mkdir(remote_path: String) { channel.mkdir(remote_path) }
   143     def mkdir(path: Path): Unit = channel.mkdir(remote_path(path))
   144     def rmdir(remote_path: String) { channel.rmdir(remote_path) }
   144     def rmdir(path: Path): Unit = channel.rmdir(remote_path(path))
   145 
   145 
   146     def stat(remote_path: String): Option[Dir_Entry] =
   146     def stat(path: Path): Option[Dir_Entry] =
   147       try { Some(Dir_Entry(remote_path, channel.stat(remote_path))) }
   147       try { Some(Dir_Entry(expand_path(path), channel.stat(remote_path(path)))) }
   148       catch { case _: SftpException => None }
   148       catch { case _: SftpException => None }
   149 
   149 
   150     def is_file(remote_path: String): Boolean = stat(remote_path).map(_.is_file) getOrElse false
   150     def is_file(path: Path): Boolean = stat(path).map(_.is_file) getOrElse false
   151     def is_dir(remote_path: String): Boolean = stat(remote_path).map(_.is_dir) getOrElse false
   151     def is_dir(path: Path): Boolean = stat(path).map(_.is_dir) getOrElse false
   152 
   152 
   153     def read_dir(remote_path: String): List[Dir_Entry] =
   153     def read_dir(path: Path): List[Dir_Entry] =
   154     {
   154     {
   155       val dir = channel.ls(remote_path)
   155       val dir = channel.ls(remote_path(path))
   156       (for {
   156       (for {
   157         i <- (0 until dir.size).iterator
   157         i <- (0 until dir.size).iterator
   158         a = dir.get(i).asInstanceOf[AnyRef]
   158         a = dir.get(i).asInstanceOf[AnyRef]
   159         name = Untyped.get[String](a, "filename")
   159         name = Untyped.get[String](a, "filename")
   160         attrs = Untyped.get[Attrs](a, "attrs")
   160         attrs = Untyped.get[Attrs](a, "attrs")
   161         if name != "." && name != ".."
   161         if name != "." && name != ".."
   162       } yield Dir_Entry(name, attrs)).toList
   162       } yield Dir_Entry(Path.basic(name), attrs)).toList
   163     }
   163     }
   164 
   164 
   165     def find_files(remote_path: String, pred: Dir_Entry => Boolean = _ => true): List[Dir_Entry] =
   165     def find_files(root: Path, pred: Dir_Entry => Boolean = _ => true): List[Dir_Entry] =
   166     {
   166     {
   167       def find(dir: String): List[Dir_Entry] =
   167       def find(dir: Path): List[Dir_Entry] =
   168         read_dir(dir).flatMap(entry =>
   168         read_dir(dir).flatMap(entry =>
   169           {
   169           {
   170             val file = dir + "/" + entry.name
   170             val file = dir + entry.name
   171             if (entry.is_dir) find(file)
   171             if (entry.is_dir) find(file)
   172             else if (pred(entry)) List(entry.copy(name = file))
   172             else if (pred(entry)) List(entry.copy(name = file))
   173             else Nil
   173             else Nil
   174           })
   174           })
   175       find(remote_path)
   175       find(root)
   176     }
   176     }
   177 
   177 
   178     def open_input(remote_path: String): InputStream = channel.get(remote_path)
   178     def open_input(path: Path): InputStream = channel.get(remote_path(path))
   179     def open_output(remote_path: String): OutputStream = channel.put(remote_path)
   179     def open_output(path: Path): OutputStream = channel.put(remote_path(path))
   180 
   180 
   181     def read_file(remote_path: String, local_path: Path): Unit =
   181     def read_file(path: Path, local_path: Path): Unit =
   182       channel.get(remote_path, File.platform_path(local_path))
   182       channel.get(remote_path(path), File.platform_path(local_path))
   183     def read_bytes(remote_path: String): Bytes =
   183     def read_bytes(path: Path): Bytes = using(open_input(path))(Bytes.read_stream(_))
   184       using(open_input(remote_path))(Bytes.read_stream(_))
   184     def read(path: Path): String = using(open_input(path))(File.read_stream(_))
   185     def read(remote_path: String): String =
   185 
   186       using(open_input(remote_path))(File.read_stream(_))
   186     def write_file(path: Path, local_path: Path): Unit =
   187 
   187       channel.put(File.platform_path(local_path), remote_path(path))
   188     def write_file(remote_path: String, local_path: Path): Unit =
   188     def write_bytes(path: Path, bytes: Bytes): Unit =
   189       channel.put(File.platform_path(local_path), remote_path)
   189       using(open_output(path))(bytes.write_stream(_))
   190     def write_bytes(remote_path: String, bytes: Bytes): Unit =
   190     def write(path: Path, text: String): Unit =
   191       using(open_output(remote_path))(bytes.write_stream(_))
   191       using(open_output(path))(stream => Bytes(text).write_stream(stream))
   192     def write(remote_path: String, text: String): Unit =
       
   193       using(open_output(remote_path))(stream => Bytes(text).write_stream(stream))
       
   194   }
   192   }
   195 
   193 
   196 
   194 
   197   /* exec channel */
   195   /* exec channel */
   198 
   196 
   315       execute("rm -r -f " + File.bash_string(remote_dir)).check
   313       execute("rm -r -f " + File.bash_string(remote_dir)).check
   316 
   314 
   317     def tmp_dir(): String =
   315     def tmp_dir(): String =
   318       execute("mktemp -d -t tmp.XXXXXXXXXX").check.out
   316       execute("mktemp -d -t tmp.XXXXXXXXXX").check.out
   319 
   317 
   320     def with_tmp_dir[A](body: String => A): A =
   318     def with_tmp_dir[A](body: Path => A): A =
   321     {
   319     {
   322       val remote_dir = tmp_dir()
   320       val remote_dir = tmp_dir()
   323       try { body(remote_dir) } finally { rm_tree(remote_dir) }
   321       try { body(Path.explode(remote_dir)) } finally { rm_tree(remote_dir) }
   324     }
   322     }
   325   }
   323   }
   326 }
   324 }
   327 
   325 
   328 class SSH private(val options: Options, val jsch: JSch)
   326 class SSH private(val options: Options, val jsch: JSch)