| author | wenzelm | 
| Mon, 28 Aug 2017 20:15:11 +0200 | |
| changeset 66530 | a3a847c4fbdb | 
| parent 65717 | 556c34fd0554 | 
| child 66570 | 9af879e222cc | 
| 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 | ||
| 65594 | 77 | def open_session(host: String, user: String = "", port: Int = 0): Session = | 
| 64257 | 78 |     {
 | 
| 65594 | 79 | val session = | 
| 65717 | 80 | jsch.getSession(proper_string(user) getOrElse null, host, | 
| 81 | if (port > 0) port else default_port) | |
| 64257 | 82 | |
| 83 | session.setUserInfo(No_User_Info) | |
| 64325 | 84 | session.setServerAliveInterval(alive_interval(options)) | 
| 64257 | 85 |       session.setConfig("MaxAuthTries", "3")
 | 
| 86 | ||
| 87 |       if (options.bool("ssh_compression")) {
 | |
| 88 |         session.setConfig("compression.s2c", "zlib@openssh.com,zlib,none")
 | |
| 89 |         session.setConfig("compression.c2s", "zlib@openssh.com,zlib,none")
 | |
| 90 |         session.setConfig("compression_level", "9")
 | |
| 91 | } | |
| 92 | ||
| 93 | session.connect(connect_timeout(options)) | |
| 94 | new Session(options, session) | |
| 95 | } | |
| 96 | } | |
| 64130 | 97 | |
| 64123 | 98 | |
| 99 | /* logging */ | |
| 100 | ||
| 101 | def logging(verbose: Boolean = true, debug: Boolean = false) | |
| 102 |   {
 | |
| 103 | JSch.setLogger(if (verbose) new Logger(debug) else null) | |
| 104 | } | |
| 105 | ||
| 106 | private class Logger(debug: Boolean) extends JSch_Logger | |
| 107 |   {
 | |
| 108 | def isEnabled(level: Int): Boolean = level != JSch_Logger.DEBUG || debug | |
| 109 | ||
| 110 | def log(level: Int, msg: String) | |
| 111 |     {
 | |
| 112 |       level match {
 | |
| 113 | case JSch_Logger.ERROR | JSch_Logger.FATAL => Output.error_message(msg) | |
| 114 | case JSch_Logger.WARN => Output.warning(msg) | |
| 115 | case _ => Output.writeln(msg) | |
| 116 | } | |
| 117 | } | |
| 118 | } | |
| 119 | ||
| 120 | ||
| 64128 | 121 | /* user info */ | 
| 122 | ||
| 123 | object No_User_Info extends UserInfo | |
| 124 |   {
 | |
| 125 | def getPassphrase: String = null | |
| 126 | def getPassword: String = null | |
| 127 | def promptPassword(msg: String): Boolean = false | |
| 128 | def promptPassphrase(msg: String): Boolean = false | |
| 129 | def promptYesNo(msg: String): Boolean = false | |
| 130 | def showMessage(msg: String): Unit = Output.writeln(msg) | |
| 131 | } | |
| 132 | ||
| 133 | ||
| 65009 | 134 | /* port forwarding */ | 
| 135 | ||
| 65010 | 136 | object Port_Forwarding | 
| 65009 | 137 |   {
 | 
| 65636 
df804cdba5f9
ssh_close for proper termination after use of database;
 wenzelm parents: 
65594diff
changeset | 138 | def open(ssh: Session, ssh_close: Boolean, | 
| 65010 | 139 | local_host: String, local_port: Int, remote_host: String, remote_port: Int): Port_Forwarding = | 
| 140 |     {
 | |
| 141 | val port = ssh.session.setPortForwardingL(local_host, local_port, remote_host, remote_port) | |
| 65636 
df804cdba5f9
ssh_close for proper termination after use of database;
 wenzelm parents: 
65594diff
changeset | 142 | new Port_Forwarding(ssh, ssh_close, local_host, port, remote_host, remote_port) | 
| 65010 | 143 | } | 
| 144 | } | |
| 145 | ||
| 146 | class Port_Forwarding private[SSH]( | |
| 147 | ssh: SSH.Session, | |
| 65636 
df804cdba5f9
ssh_close for proper termination after use of database;
 wenzelm parents: 
65594diff
changeset | 148 | ssh_close: Boolean, | 
| 65010 | 149 | val local_host: String, | 
| 150 | val local_port: Int, | |
| 151 | val remote_host: String, | |
| 152 | val remote_port: Int) | |
| 153 |   {
 | |
| 154 | override def toString: String = | |
| 155 | local_host + ":" + local_port + ":" + remote_host + ":" + remote_port | |
| 156 | ||
| 65636 
df804cdba5f9
ssh_close for proper termination after use of database;
 wenzelm parents: 
65594diff
changeset | 157 | def close() | 
| 
df804cdba5f9
ssh_close for proper termination after use of database;
 wenzelm parents: 
65594diff
changeset | 158 |     {
 | 
| 
df804cdba5f9
ssh_close for proper termination after use of database;
 wenzelm parents: 
65594diff
changeset | 159 | ssh.session.delPortForwardingL(local_host, local_port) | 
| 
df804cdba5f9
ssh_close for proper termination after use of database;
 wenzelm parents: 
65594diff
changeset | 160 | if (ssh_close) ssh.close() | 
| 
df804cdba5f9
ssh_close for proper termination after use of database;
 wenzelm parents: 
65594diff
changeset | 161 | } | 
| 65009 | 162 | } | 
| 163 | ||
| 164 | ||
| 64191 | 165 | /* Sftp channel */ | 
| 166 | ||
| 167 | type Attrs = SftpATTRS | |
| 168 | ||
| 64233 | 169 | sealed case class Dir_Entry(name: Path, attrs: Attrs) | 
| 64191 | 170 |   {
 | 
| 171 | def is_file: Boolean = attrs.isReg | |
| 172 | def is_dir: Boolean = attrs.isDir | |
| 173 | } | |
| 174 | ||
| 175 | ||
| 64132 | 176 | /* exec channel */ | 
| 177 | ||
| 64134 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 178 | private val exec_wait_delay = Time.seconds(0.3) | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 179 | |
| 64256 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 180 | class Exec private[SSH](session: Session, channel: ChannelExec) | 
| 64131 | 181 |   {
 | 
| 64256 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 182 | 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 | 183 | |
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 184 |     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 | 185 | |
| 64134 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 186 | val exit_status: Future[Int] = | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 187 |       Future.thread("ssh_wait") {
 | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 188 | while (!channel.isClosed) Thread.sleep(exec_wait_delay.ms) | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 189 | channel.getExitStatus | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 190 | } | 
| 
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 | val stdin: OutputStream = channel.getOutputStream | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 193 | val stdout: InputStream = channel.getInputStream | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 194 | val stderr: InputStream = channel.getErrStream | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 195 | |
| 64166 | 196 | // connect after preparing streams | 
| 197 | channel.connect(connect_timeout(session.options)) | |
| 64134 
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 result( | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 200 | progress_stdout: String => Unit = (_: String) => (), | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 201 | progress_stderr: String => Unit = (_: String) => (), | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 202 | strict: Boolean = true): Process_Result = | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 203 |     {
 | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 204 | stdin.close | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 205 | |
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 206 | def read_lines(stream: InputStream, progress: String => Unit): List[String] = | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 207 |       {
 | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 208 | val result = new mutable.ListBuffer[String] | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 209 | val line_buffer = new ByteArrayOutputStream(100) | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 210 | def line_flush() | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 211 |         {
 | 
| 64326 | 212 | 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 | 213 | progress(line) | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 214 | result += line | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 215 | line_buffer.reset | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 216 | } | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 217 | |
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 218 | var c = 0 | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 219 | var finished = false | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 220 |         while (!finished) {
 | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 221 |           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 | 222 | if (c == 10) line_flush() | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 223 |           else if (channel.isClosed) {
 | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 224 | if (line_buffer.size > 0) line_flush() | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 225 | finished = true | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 226 | } | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 227 | else Thread.sleep(exec_wait_delay.ms) | 
| 
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 | |
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 230 | result.toList | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 231 | } | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 232 | |
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 233 |       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 | 234 |       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 | 235 | |
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 236 | def terminate() | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 237 |       {
 | 
| 64136 | 238 | close | 
| 64134 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 239 | out_lines.join | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 240 | err_lines.join | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 241 | exit_status.join | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 242 | } | 
| 
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 | val rc = | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 245 |         try { exit_status.join }
 | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 246 |         catch { case Exn.Interrupt() => terminate(); Exn.Interrupt.return_code }
 | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 247 | |
| 64136 | 248 | close | 
| 64134 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 249 | if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt() | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 250 | |
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 251 | Process_Result(rc, out_lines.join, err_lines.join) | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 252 | } | 
| 64131 | 253 | } | 
| 254 | ||
| 255 | ||
| 64123 | 256 | /* session */ | 
| 257 | ||
| 64166 | 258 | class Session private[SSH](val options: Options, val session: JSch_Session) | 
| 64123 | 259 |   {
 | 
| 64166 | 260 | def update_options(new_options: Options): Session = new Session(new_options, session) | 
| 261 | ||
| 64347 | 262 | def user_prefix: String = if (session.getUserName == null) "" else session.getUserName + "@" | 
| 263 | def host: String = if (session.getHost == null) "" else session.getHost | |
| 264 | def port_suffix: String = if (session.getPort == default_port) "" else ":" + session.getPort | |
| 265 | def hg_url: String = "ssh://" + user_prefix + host + port_suffix + "/" | |
| 266 | ||
| 64123 | 267 | override def toString: String = | 
| 64347 | 268 | user_prefix + host + port_suffix + (if (session.isConnected) "" else " (disconnected)") | 
| 64123 | 269 | |
| 64256 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 270 | |
| 65009 | 271 | /* port forwarding */ | 
| 272 | ||
| 65636 
df804cdba5f9
ssh_close for proper termination after use of database;
 wenzelm parents: 
65594diff
changeset | 273 | def port_forwarding( | 
| 
df804cdba5f9
ssh_close for proper termination after use of database;
 wenzelm parents: 
65594diff
changeset | 274 | remote_port: Int, remote_host: String = "localhost", | 
| 
df804cdba5f9
ssh_close for proper termination after use of database;
 wenzelm parents: 
65594diff
changeset | 275 | local_port: Int = 0, local_host: String = "localhost", | 
| 
df804cdba5f9
ssh_close for proper termination after use of database;
 wenzelm parents: 
65594diff
changeset | 276 | ssh_close: Boolean = false): Port_Forwarding = | 
| 
df804cdba5f9
ssh_close for proper termination after use of database;
 wenzelm parents: 
65594diff
changeset | 277 | Port_Forwarding.open(this, ssh_close, local_host, local_port, remote_host, remote_port) | 
| 65009 | 278 | |
| 279 | ||
| 64256 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 280 | /* sftp channel */ | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 281 | |
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 282 |     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 | 283 | 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 | 284 | |
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 285 |     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 | 286 | |
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 287 | 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 | 288 |     {
 | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 289 | 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 | 290 |       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 | 291 | } | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 292 | 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 | 293 | def remote_path(path: Path): String = expand_path(path).implode | 
| 64304 | 294 | def bash_path(path: Path): String = Bash.string(remote_path(path)) | 
| 64123 | 295 | |
| 64256 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 296 | 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 | 297 | 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 | 298 | 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 | 299 | 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 | 300 | 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 | 301 | |
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 302 | 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 | 303 |       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 | 304 |       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 | 305 | |
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 306 | 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 | 307 | 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 | 308 | |
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 309 | 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 | 310 |       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 | 311 | execute( | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 312 |           "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 | 313 |         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 | 314 | } | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 315 | |
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 316 | def read_dir(path: Path): List[Dir_Entry] = | 
| 64191 | 317 |     {
 | 
| 64256 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 318 | 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 | 319 |       (for {
 | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 320 | 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 | 321 | 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 | 322 | 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 | 323 | 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 | 324 | if name != "." && name != ".." | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 325 | } yield Dir_Entry(Path.basic(name), attrs)).toList | 
| 64191 | 326 | } | 
| 64135 
865dda40e1cc
provide execute operation, similar to Isabelle_System.bash;
 wenzelm parents: 
64134diff
changeset | 327 | |
| 64256 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 328 | 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 | 329 |     {
 | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 330 | 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 | 331 | 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 | 332 |           {
 | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 333 | 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 | 334 | 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 | 335 | 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 | 336 | else Nil | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 337 | }) | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 338 | find(root) | 
| 
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 | |
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 341 | 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 | 342 | 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 | 343 | |
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 344 | 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 | 345 | 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 | 346 | 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 | 347 | 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 | 348 | |
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 349 | 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 | 350 | 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 | 351 | 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 | 352 | 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 | 353 | 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 | 354 | 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 | 355 | |
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 356 | |
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 357 | /* exec channel */ | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 358 | |
| 64166 | 359 | def exec(command: String): Exec = | 
| 64129 | 360 |     {
 | 
| 64256 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 361 |       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 | 362 |       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 | 363 | new Exec(this, channel) | 
| 64129 | 364 | } | 
| 64123 | 365 | |
| 64191 | 366 | def execute(command: String, | 
| 367 | progress_stdout: String => Unit = (_: String) => (), | |
| 368 | progress_stderr: String => Unit = (_: String) => (), | |
| 369 | strict: Boolean = true): Process_Result = | |
| 370 | exec(command).result(progress_stdout, progress_stderr, strict) | |
| 64137 | 371 | |
| 372 | ||
| 373 | /* tmp dirs */ | |
| 374 | ||
| 64306 
7b6dc1b36f20
tuned signature, in accordance to Isabelle_System;
 wenzelm parents: 
64304diff
changeset | 375 | def rm_tree(dir: Path): Unit = rm_tree(remote_path(dir)) | 
| 
7b6dc1b36f20
tuned signature, in accordance to Isabelle_System;
 wenzelm parents: 
64304diff
changeset | 376 | |
| 64137 | 377 | def rm_tree(remote_dir: String): Unit = | 
| 64304 | 378 |       execute("rm -r -f " + Bash.string(remote_dir)).check
 | 
| 64137 | 379 | |
| 380 | def tmp_dir(): String = | |
| 381 |       execute("mktemp -d -t tmp.XXXXXXXXXX").check.out
 | |
| 382 | ||
| 64233 | 383 | def with_tmp_dir[A](body: Path => A): A = | 
| 64137 | 384 |     {
 | 
| 385 | val remote_dir = tmp_dir() | |
| 64233 | 386 |       try { body(Path.explode(remote_dir)) } finally { rm_tree(remote_dir) }
 | 
| 64137 | 387 | } | 
| 64123 | 388 | } | 
| 389 | } |