| author | wenzelm | 
| Sat, 04 Mar 2017 08:41:32 +0100 | |
| changeset 65100 | 83d1f210a1d3 | 
| parent 65010 | a27e9908dcf7 | 
| child 65594 | 659305708959 | 
| permissions | -rw-r--r-- | 
| 64123 | 1 | /* Title: Pure/General/ssh.scala | 
| 2 | Author: Makarius | |
| 3 | ||
| 64124 | 4 | SSH client based on JSch (see also http://www.jcraft.com/jsch/examples). | 
| 64123 | 5 | */ | 
| 6 | ||
| 7 | package isabelle | |
| 8 | ||
| 9 | ||
| 64134 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 10 | import java.io.{InputStream, OutputStream, ByteArrayOutputStream}
 | 
| 64131 | 11 | |
| 64134 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 12 | import scala.collection.{mutable, JavaConversions}
 | 
| 64131 | 13 | |
| 64222 | 14 | import com.jcraft.jsch.{JSch, Logger => JSch_Logger, Session => JSch_Session, SftpException,
 | 
| 64132 | 15 | OpenSSHConfig, UserInfo, Channel => JSch_Channel, ChannelExec, ChannelSftp, SftpATTRS} | 
| 64123 | 16 | |
| 17 | ||
| 18 | object SSH | |
| 19 | {
 | |
| 64185 | 20 | /* target machine: user@host syntax */ | 
| 64141 | 21 | |
| 64185 | 22 | object Target | 
| 64141 | 23 |   {
 | 
| 24 | val Pattern = "^([^@]+)@(.+)$".r | |
| 25 | ||
| 26 | def parse(s: String): (String, String) = | |
| 27 |       s match {
 | |
| 28 | case Pattern(user, host) => (user, host) | |
| 29 |         case _ => ("", s)
 | |
| 30 | } | |
| 31 | ||
| 32 | def unapplySeq(s: String): Option[List[String]] = | |
| 64185 | 33 |       parse(s) match {
 | 
| 34 | case (_, "") => None | |
| 35 | case (user, host) => Some(List(user, host)) | |
| 36 | } | |
| 64141 | 37 | } | 
| 38 | ||
| 64142 | 39 | val default_port = 22 | 
| 40 | ||
| 64257 | 41 | def connect_timeout(options: Options): Int = | 
| 42 |     options.seconds("ssh_connect_timeout").ms.toInt
 | |
| 64141 | 43 | |
| 64325 | 44 | def alive_interval(options: Options): Int = | 
| 45 |     options.seconds("ssh_alive_interval").ms.toInt
 | |
| 46 | ||
| 64123 | 47 | |
| 64257 | 48 | /* init context */ | 
| 49 | ||
| 50 | def init_context(options: Options): Context = | |
| 64123 | 51 |   {
 | 
| 64130 | 52 |     val config_dir = Path.explode(options.string("ssh_config_dir"))
 | 
| 64123 | 53 |     if (!config_dir.is_dir) error("Bad ssh config directory: " + config_dir)
 | 
| 54 | ||
| 55 | val jsch = new JSch | |
| 56 | ||
| 64130 | 57 |     val config_file = Path.explode(options.string("ssh_config_file"))
 | 
| 64123 | 58 | if (config_file.is_file) | 
| 59 | jsch.setConfigRepository(OpenSSHConfig.parseFile(File.platform_path(config_file))) | |
| 60 | ||
| 61 |     val known_hosts = config_dir + Path.explode("known_hosts")
 | |
| 62 | if (!known_hosts.is_file) known_hosts.file.createNewFile | |
| 63 | jsch.setKnownHosts(File.platform_path(known_hosts)) | |
| 64 | ||
| 64130 | 65 | val identity_files = | 
| 66 |       Library.space_explode(':', options.string("ssh_identity_files")).map(Path.explode(_))
 | |
| 64123 | 67 | for (identity_file <- identity_files if identity_file.is_file) | 
| 68 | jsch.addIdentity(File.platform_path(identity_file)) | |
| 69 | ||
| 64257 | 70 | new Context(options, jsch) | 
| 64123 | 71 | } | 
| 72 | ||
| 64257 | 73 | class Context private[SSH](val options: Options, val jsch: JSch) | 
| 74 |   {
 | |
| 75 | def update_options(new_options: Options): Context = new Context(new_options, jsch) | |
| 76 | ||
| 77 | def open_session(host: String, user: String = "", port: Int = default_port): Session = | |
| 78 |     {
 | |
| 79 | val session = jsch.getSession(if (user == "") null else user, host, port) | |
| 80 | ||
| 81 | session.setUserInfo(No_User_Info) | |
| 64325 | 82 | session.setServerAliveInterval(alive_interval(options)) | 
| 64257 | 83 |       session.setConfig("MaxAuthTries", "3")
 | 
| 84 | ||
| 85 |       if (options.bool("ssh_compression")) {
 | |
| 86 |         session.setConfig("compression.s2c", "zlib@openssh.com,zlib,none")
 | |
| 87 |         session.setConfig("compression.c2s", "zlib@openssh.com,zlib,none")
 | |
| 88 |         session.setConfig("compression_level", "9")
 | |
| 89 | } | |
| 90 | ||
| 91 | session.connect(connect_timeout(options)) | |
| 92 | new Session(options, session) | |
| 93 | } | |
| 94 | } | |
| 64130 | 95 | |
| 64123 | 96 | |
| 97 | /* logging */ | |
| 98 | ||
| 99 | def logging(verbose: Boolean = true, debug: Boolean = false) | |
| 100 |   {
 | |
| 101 | JSch.setLogger(if (verbose) new Logger(debug) else null) | |
| 102 | } | |
| 103 | ||
| 104 | private class Logger(debug: Boolean) extends JSch_Logger | |
| 105 |   {
 | |
| 106 | def isEnabled(level: Int): Boolean = level != JSch_Logger.DEBUG || debug | |
| 107 | ||
| 108 | def log(level: Int, msg: String) | |
| 109 |     {
 | |
| 110 |       level match {
 | |
| 111 | case JSch_Logger.ERROR | JSch_Logger.FATAL => Output.error_message(msg) | |
| 112 | case JSch_Logger.WARN => Output.warning(msg) | |
| 113 | case _ => Output.writeln(msg) | |
| 114 | } | |
| 115 | } | |
| 116 | } | |
| 117 | ||
| 118 | ||
| 64128 | 119 | /* user info */ | 
| 120 | ||
| 121 | object No_User_Info extends UserInfo | |
| 122 |   {
 | |
| 123 | def getPassphrase: String = null | |
| 124 | def getPassword: String = null | |
| 125 | def promptPassword(msg: String): Boolean = false | |
| 126 | def promptPassphrase(msg: String): Boolean = false | |
| 127 | def promptYesNo(msg: String): Boolean = false | |
| 128 | def showMessage(msg: String): Unit = Output.writeln(msg) | |
| 129 | } | |
| 130 | ||
| 131 | ||
| 65009 | 132 | /* port forwarding */ | 
| 133 | ||
| 65010 | 134 | object Port_Forwarding | 
| 65009 | 135 |   {
 | 
| 65010 | 136 | def open(ssh: Session, | 
| 137 | local_host: String, local_port: Int, remote_host: String, remote_port: Int): Port_Forwarding = | |
| 138 |     {
 | |
| 139 | val port = ssh.session.setPortForwardingL(local_host, local_port, remote_host, remote_port) | |
| 140 | new Port_Forwarding(ssh, local_host, port, remote_host, remote_port) | |
| 141 | } | |
| 142 | } | |
| 143 | ||
| 144 | class Port_Forwarding private[SSH]( | |
| 145 | ssh: SSH.Session, | |
| 146 | val local_host: String, | |
| 147 | val local_port: Int, | |
| 148 | val remote_host: String, | |
| 149 | val remote_port: Int) | |
| 150 |   {
 | |
| 151 | override def toString: String = | |
| 152 | local_host + ":" + local_port + ":" + remote_host + ":" + remote_port | |
| 153 | ||
| 154 |     def close() { ssh.session.delPortForwardingL(local_host, local_port) }
 | |
| 65009 | 155 | } | 
| 156 | ||
| 157 | ||
| 64191 | 158 | /* Sftp channel */ | 
| 159 | ||
| 160 | type Attrs = SftpATTRS | |
| 161 | ||
| 64233 | 162 | sealed case class Dir_Entry(name: Path, attrs: Attrs) | 
| 64191 | 163 |   {
 | 
| 164 | def is_file: Boolean = attrs.isReg | |
| 165 | def is_dir: Boolean = attrs.isDir | |
| 166 | } | |
| 167 | ||
| 168 | ||
| 64132 | 169 | /* exec channel */ | 
| 170 | ||
| 64134 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 171 | private val exec_wait_delay = Time.seconds(0.3) | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 172 | |
| 64256 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 173 | class Exec private[SSH](session: Session, channel: ChannelExec) | 
| 64131 | 174 |   {
 | 
| 64256 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 175 | override def toString: String = "exec " + session.toString | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 176 | |
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 177 |     def close() { channel.disconnect }
 | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 178 | |
| 64134 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 179 | val exit_status: Future[Int] = | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 180 |       Future.thread("ssh_wait") {
 | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 181 | while (!channel.isClosed) Thread.sleep(exec_wait_delay.ms) | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 182 | channel.getExitStatus | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 183 | } | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 184 | |
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 185 | val stdin: OutputStream = channel.getOutputStream | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 186 | val stdout: InputStream = channel.getInputStream | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 187 | val stderr: InputStream = channel.getErrStream | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 188 | |
| 64166 | 189 | // connect after preparing streams | 
| 190 | channel.connect(connect_timeout(session.options)) | |
| 64134 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 191 | |
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 192 | def result( | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 193 | progress_stdout: String => Unit = (_: String) => (), | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 194 | progress_stderr: String => Unit = (_: String) => (), | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 195 | strict: Boolean = true): Process_Result = | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 196 |     {
 | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 197 | stdin.close | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 198 | |
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 199 | def read_lines(stream: InputStream, progress: String => Unit): List[String] = | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 200 |       {
 | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 201 | val result = new mutable.ListBuffer[String] | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 202 | val line_buffer = new ByteArrayOutputStream(100) | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 203 | def line_flush() | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 204 |         {
 | 
| 64326 | 205 | val line = Library.trim_line(line_buffer.toString(UTF8.charset_name)) | 
| 64134 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 206 | progress(line) | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 207 | result += line | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 208 | line_buffer.reset | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 209 | } | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 210 | |
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 211 | var c = 0 | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 212 | var finished = false | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 213 |         while (!finished) {
 | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 214 |           while ({ c = stream.read; c != -1 && c != 10 }) line_buffer.write(c)
 | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 215 | if (c == 10) line_flush() | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 216 |           else if (channel.isClosed) {
 | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 217 | if (line_buffer.size > 0) line_flush() | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 218 | finished = true | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 219 | } | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 220 | else Thread.sleep(exec_wait_delay.ms) | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 221 | } | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 222 | |
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 223 | result.toList | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 224 | } | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 225 | |
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 226 |       val out_lines = Future.thread("ssh_stdout") { read_lines(stdout, progress_stdout) }
 | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 227 |       val err_lines = Future.thread("ssh_stderr") { read_lines(stderr, progress_stderr) }
 | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 228 | |
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 229 | def terminate() | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 230 |       {
 | 
| 64136 | 231 | close | 
| 64134 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 232 | out_lines.join | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 233 | err_lines.join | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 234 | exit_status.join | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 235 | } | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 236 | |
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 237 | val rc = | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 238 |         try { exit_status.join }
 | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 239 |         catch { case Exn.Interrupt() => terminate(); Exn.Interrupt.return_code }
 | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 240 | |
| 64136 | 241 | close | 
| 64134 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 242 | if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt() | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 243 | |
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 244 | Process_Result(rc, out_lines.join, err_lines.join) | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 245 | } | 
| 64131 | 246 | } | 
| 247 | ||
| 248 | ||
| 64123 | 249 | /* session */ | 
| 250 | ||
| 64166 | 251 | class Session private[SSH](val options: Options, val session: JSch_Session) | 
| 64123 | 252 |   {
 | 
| 64166 | 253 | def update_options(new_options: Options): Session = new Session(new_options, session) | 
| 254 | ||
| 64347 | 255 | def user_prefix: String = if (session.getUserName == null) "" else session.getUserName + "@" | 
| 256 | def host: String = if (session.getHost == null) "" else session.getHost | |
| 257 | def port_suffix: String = if (session.getPort == default_port) "" else ":" + session.getPort | |
| 258 | def hg_url: String = "ssh://" + user_prefix + host + port_suffix + "/" | |
| 259 | ||
| 64123 | 260 | override def toString: String = | 
| 64347 | 261 | user_prefix + host + port_suffix + (if (session.isConnected) "" else " (disconnected)") | 
| 64123 | 262 | |
| 64256 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 263 | |
| 65009 | 264 | /* port forwarding */ | 
| 265 | ||
| 65010 | 266 | def port_forwarding(remote_port: Int, remote_host: String = "localhost", | 
| 65009 | 267 | local_port: Int = 0, local_host: String = "localhost"): Port_Forwarding = | 
| 65010 | 268 | Port_Forwarding.open(this, local_host, local_port, remote_host, remote_port) | 
| 65009 | 269 | |
| 270 | ||
| 64256 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 271 | /* sftp channel */ | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 272 | |
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 273 |     val sftp: ChannelSftp = session.openChannel("sftp").asInstanceOf[ChannelSftp]
 | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 274 | sftp.connect(connect_timeout(options)) | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 275 | |
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 276 |     def close() { sftp.disconnect; session.disconnect }
 | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 277 | |
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 278 | val settings: Map[String, String] = | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 279 |     {
 | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 280 | val home = sftp.getHome | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 281 |       Map("HOME" -> home, "USER_HOME" -> home)
 | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 282 | } | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 283 | def expand_path(path: Path): Path = path.expand_env(settings) | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 284 | def remote_path(path: Path): String = expand_path(path).implode | 
| 64304 | 285 | def bash_path(path: Path): String = Bash.string(remote_path(path)) | 
| 64123 | 286 | |
| 64256 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 287 | def chmod(permissions: Int, path: Path): Unit = sftp.chmod(permissions, remote_path(path)) | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 288 | def mv(path1: Path, path2: Path): Unit = sftp.rename(remote_path(path1), remote_path(path2)) | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 289 | def rm(path: Path): Unit = sftp.rm(remote_path(path)) | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 290 | def mkdir(path: Path): Unit = sftp.mkdir(remote_path(path)) | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 291 | def rmdir(path: Path): Unit = sftp.rmdir(remote_path(path)) | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 292 | |
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 293 | def stat(path: Path): Option[Dir_Entry] = | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 294 |       try { Some(Dir_Entry(expand_path(path), sftp.stat(remote_path(path)))) }
 | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 295 |       catch { case _: SftpException => None }
 | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 296 | |
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 297 | def is_file(path: Path): Boolean = stat(path).map(_.is_file) getOrElse false | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 298 | def is_dir(path: Path): Boolean = stat(path).map(_.is_dir) getOrElse false | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 299 | |
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 300 | def mkdirs(path: Path): Unit = | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 301 |       if (!is_dir(path)) {
 | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 302 | execute( | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 303 |           "perl -e \"use File::Path make_path; make_path('" + remote_path(path) + "');\"")
 | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 304 |         if (!is_dir(path)) error("Failed to create directory: " + quote(remote_path(path)))
 | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 305 | } | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 306 | |
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 307 | def read_dir(path: Path): List[Dir_Entry] = | 
| 64191 | 308 |     {
 | 
| 64256 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 309 | val dir = sftp.ls(remote_path(path)) | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 310 |       (for {
 | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 311 | i <- (0 until dir.size).iterator | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 312 | a = dir.get(i).asInstanceOf[AnyRef] | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 313 | name = Untyped.get[String](a, "filename") | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 314 | attrs = Untyped.get[Attrs](a, "attrs") | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 315 | if name != "." && name != ".." | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 316 | } yield Dir_Entry(Path.basic(name), attrs)).toList | 
| 64191 | 317 | } | 
| 64135 
865dda40e1cc
provide execute operation, similar to Isabelle_System.bash;
 wenzelm parents: 
64134diff
changeset | 318 | |
| 64256 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 319 | def find_files(root: Path, pred: Dir_Entry => Boolean = _ => true): List[Dir_Entry] = | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 320 |     {
 | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 321 | def find(dir: Path): List[Dir_Entry] = | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 322 | read_dir(dir).flatMap(entry => | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 323 |           {
 | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 324 | val file = dir + entry.name | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 325 | if (entry.is_dir) find(file) | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 326 | else if (pred(entry)) List(entry.copy(name = file)) | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 327 | else Nil | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 328 | }) | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 329 | find(root) | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 330 | } | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 331 | |
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 332 | def open_input(path: Path): InputStream = sftp.get(remote_path(path)) | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 333 | def open_output(path: Path): OutputStream = sftp.put(remote_path(path)) | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 334 | |
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 335 | def read_file(path: Path, local_path: Path): Unit = | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 336 | sftp.get(remote_path(path), File.platform_path(local_path)) | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 337 | def read_bytes(path: Path): Bytes = using(open_input(path))(Bytes.read_stream(_)) | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 338 | def read(path: Path): String = using(open_input(path))(File.read_stream(_)) | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 339 | |
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 340 | def write_file(path: Path, local_path: Path): Unit = | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 341 | sftp.put(File.platform_path(local_path), remote_path(path)) | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 342 | def write_bytes(path: Path, bytes: Bytes): Unit = | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 343 | using(open_output(path))(bytes.write_stream(_)) | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 344 | def write(path: Path, text: String): Unit = | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 345 | using(open_output(path))(stream => Bytes(text).write_stream(stream)) | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 346 | |
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 347 | |
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 348 | /* exec channel */ | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 349 | |
| 64166 | 350 | def exec(command: String): Exec = | 
| 64129 | 351 |     {
 | 
| 64256 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 352 |       val channel = session.openChannel("exec").asInstanceOf[ChannelExec]
 | 
| 64190 
c62b99e3ec07
provide USER_HOME, such that symbolic Path.explode("~") can be used remotely;
 wenzelm parents: 
64185diff
changeset | 353 |       channel.setCommand("export USER_HOME=\"$HOME\"\n" + command)
 | 
| 64256 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 354 | new Exec(this, channel) | 
| 64129 | 355 | } | 
| 64123 | 356 | |
| 64191 | 357 | def execute(command: String, | 
| 358 | progress_stdout: String => Unit = (_: String) => (), | |
| 359 | progress_stderr: String => Unit = (_: String) => (), | |
| 360 | strict: Boolean = true): Process_Result = | |
| 361 | exec(command).result(progress_stdout, progress_stderr, strict) | |
| 64137 | 362 | |
| 363 | ||
| 364 | /* tmp dirs */ | |
| 365 | ||
| 64306 
7b6dc1b36f20
tuned signature, in accordance to Isabelle_System;
 wenzelm parents: 
64304diff
changeset | 366 | def rm_tree(dir: Path): Unit = rm_tree(remote_path(dir)) | 
| 
7b6dc1b36f20
tuned signature, in accordance to Isabelle_System;
 wenzelm parents: 
64304diff
changeset | 367 | |
| 64137 | 368 | def rm_tree(remote_dir: String): Unit = | 
| 64304 | 369 |       execute("rm -r -f " + Bash.string(remote_dir)).check
 | 
| 64137 | 370 | |
| 371 | def tmp_dir(): String = | |
| 372 |       execute("mktemp -d -t tmp.XXXXXXXXXX").check.out
 | |
| 373 | ||
| 64233 | 374 | def with_tmp_dir[A](body: Path => A): A = | 
| 64137 | 375 |     {
 | 
| 376 | val remote_dir = tmp_dir() | |
| 64233 | 377 |       try { body(Path.explode(remote_dir)) } finally { rm_tree(remote_dir) }
 | 
| 64137 | 378 | } | 
| 64123 | 379 | } | 
| 380 | } |