Pure/General/ssh.scala

334     override def expand_path(path: Path): Path = path.expand_env(settings)
335     def remote_path(path: Path): String = expand_path(path).implode
336     override def bash_path(path: Path): String = Bash.string(remote_path(path))
338     def chmod(permissions: Int, path: Path): Unit = sftp.chmod(permissions, remote_path(path))
340     def rm(path: Path): Unit = sftp.rm(remote_path(path))
341     def mkdir(path: Path): Unit = sftp.mkdir(remote_path(path))
342     def rmdir(path: Path): Unit = sftp.rmdir(remote_path(path))
344     def stat(path: Path): Option[Dir_Entry] =
345       try { Some(Dir_Entry(expand_path(path), sftp.stat(remote_path(path)))) }
348     override def is_file(path: Path): Boolean = stat(path).map(_.is_file) getOrElse false
349     override def is_dir(path: Path): Boolean = stat(path).map(_.is_dir) getOrElse false
351     override def mkdirs(path: Path): Unit =
352       if (!is_dir(path)) {
354           "perl -e \"use File::Path make_path; make_path('" + remote_path(path) + "');\"")
355         if (!is_dir(path)) error("Failed to create directory: " + quote(remote_path(path)))
358     def read_dir(path: Path): List[Dir_Entry] =
360       val dir = sftp.ls(remote_path(path))
383     def open_input(path: Path): InputStream = sftp.get(remote_path(path))
384     def open_output(path: Path): OutputStream = sftp.put(remote_path(path))
386     def read_file(path: Path, local_path: Path): Unit =
387       sftp.get(remote_path(path), File.platform_path(local_path))
388     def read_bytes(path: Path): Bytes = using(open_input(path))(Bytes.read_stream(_))
389     def read(path: Path): String = using(open_input(path))(File.read_stream(_))
391     def write_file(path: Path, local_path: Path): Unit =
392       sftp.put(File.platform_path(local_path), remote_path(path))
393     def write_bytes(path: Path, bytes: Bytes): Unit =
394       using(open_output(path))(bytes.write_stream(_))
395     def write(path: Path, text: String): Unit =
396       using(open_output(path))(stream => Bytes(text).write_stream(stream))
441     def expand_path(path: Path): Path = path.expand
442     def bash_path(path: Path): String = File.bash_path(path)
443     def is_file(path: Path): Boolean = path.is_file
444     def is_dir(path: Path): Boolean = path.is_dir
445     def mkdirs(path: Path): Unit = Isabelle_System.mkdirs(path)