| author | wenzelm | 
| Sun, 24 May 2020 12:38:41 +0200 | |
| changeset 71876 | ad063ac1f617 | 
| parent 71780 | 21adf2ed442c | 
| child 72338 | 54871a086193 | 
| 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 | |
| 71358 | 12 | import scala.collection.mutable | 
| 71601 | 13 | import scala.util.matching.Regex | 
| 64131 | 14 | |
| 64222 | 15 | import com.jcraft.jsch.{JSch, Logger => JSch_Logger, Session => JSch_Session, SftpException,
 | 
| 71780 | 16 | OpenSSHConfig, UserInfo, Channel => JSch_Channel, ChannelExec, ChannelSftp, SftpATTRS, | 
| 17 | JSchException} | |
| 64123 | 18 | |
| 19 | ||
| 20 | object SSH | |
| 21 | {
 | |
| 64185 | 22 | /* target machine: user@host syntax */ | 
| 64141 | 23 | |
| 64185 | 24 | object Target | 
| 64141 | 25 |   {
 | 
| 71601 | 26 | val User_Host: Regex = "^([^@]+)@(.+)$".r | 
| 64141 | 27 | |
| 28 | def parse(s: String): (String, String) = | |
| 29 |       s match {
 | |
| 71307 | 30 | case User_Host(user, host) => (user, host) | 
| 64141 | 31 |         case _ => ("", s)
 | 
| 32 | } | |
| 33 | ||
| 34 | def unapplySeq(s: String): Option[List[String]] = | |
| 64185 | 35 |       parse(s) match {
 | 
| 36 | case (_, "") => None | |
| 37 | case (user, host) => Some(List(user, host)) | |
| 38 | } | |
| 64141 | 39 | } | 
| 40 | ||
| 64142 | 41 | val default_port = 22 | 
| 67745 
d83efbe52438
support for proxy connection, similar to ProxyCommand in ssh config;
 wenzelm parents: 
67273diff
changeset | 42 | def make_port(port: Int): Int = if (port > 0) port else default_port | 
| 64142 | 43 | |
| 71549 | 44 | def port_suffix(port: Int): String = | 
| 45 | if (port == default_port) "" else ":" + port | |
| 46 | ||
| 47 | def user_prefix(user: String): String = | |
| 48 |     proper_string(user) match {
 | |
| 49 | case None => "" | |
| 50 | case Some(name) => name + "@" | |
| 51 | } | |
| 52 | ||
| 64257 | 53 | def connect_timeout(options: Options): Int = | 
| 54 |     options.seconds("ssh_connect_timeout").ms.toInt
 | |
| 64141 | 55 | |
| 64325 | 56 | def alive_interval(options: Options): Int = | 
| 57 |     options.seconds("ssh_alive_interval").ms.toInt
 | |
| 58 | ||
| 67273 
c573cfb2c407
more robust connection: prefer ServerAliveCountMax=3 (ssh default) instead of 1 (jsch default);
 wenzelm parents: 
67067diff
changeset | 59 | def alive_count_max(options: Options): Int = | 
| 
c573cfb2c407
more robust connection: prefer ServerAliveCountMax=3 (ssh default) instead of 1 (jsch default);
 wenzelm parents: 
67067diff
changeset | 60 |     options.int("ssh_alive_count_max")
 | 
| 
c573cfb2c407
more robust connection: prefer ServerAliveCountMax=3 (ssh default) instead of 1 (jsch default);
 wenzelm parents: 
67067diff
changeset | 61 | |
| 64123 | 62 | |
| 64257 | 63 | /* init context */ | 
| 64 | ||
| 65 | def init_context(options: Options): Context = | |
| 64123 | 66 |   {
 | 
| 64130 | 67 |     val config_dir = Path.explode(options.string("ssh_config_dir"))
 | 
| 64123 | 68 |     if (!config_dir.is_dir) error("Bad ssh config directory: " + config_dir)
 | 
| 69 | ||
| 70 | val jsch = new JSch | |
| 71 | ||
| 64130 | 72 |     val config_file = Path.explode(options.string("ssh_config_file"))
 | 
| 64123 | 73 | if (config_file.is_file) | 
| 74 | jsch.setConfigRepository(OpenSSHConfig.parseFile(File.platform_path(config_file))) | |
| 75 | ||
| 76 |     val known_hosts = config_dir + Path.explode("known_hosts")
 | |
| 77 | if (!known_hosts.is_file) known_hosts.file.createNewFile | |
| 78 | jsch.setKnownHosts(File.platform_path(known_hosts)) | |
| 79 | ||
| 64130 | 80 | val identity_files = | 
| 71601 | 81 |       space_explode(':', options.string("ssh_identity_files")).map(Path.explode)
 | 
| 71780 | 82 |     for (identity_file <- identity_files if identity_file.is_file) {
 | 
| 83 |       try { jsch.addIdentity(File.platform_path(identity_file)) }
 | |
| 84 |       catch {
 | |
| 85 | case exn: JSchException => | |
| 86 |           error("Error in ssh identity file " + identity_file + ": " + exn.getMessage)
 | |
| 87 | } | |
| 88 | } | |
| 64123 | 89 | |
| 64257 | 90 | new Context(options, jsch) | 
| 64123 | 91 | } | 
| 92 | ||
| 71564 
03133befa33b
support actual_host for lrzcloud2: the proxy_host/sshd cannot resolve invented hostname (amending 1d8b6c2253e6);
 wenzelm parents: 
71562diff
changeset | 93 | def open_session(options: Options, | 
| 
03133befa33b
support actual_host for lrzcloud2: the proxy_host/sshd cannot resolve invented hostname (amending 1d8b6c2253e6);
 wenzelm parents: 
71562diff
changeset | 94 | host: String, user: String = "", port: Int = 0, actual_host: String = "", | 
| 67771 | 95 | proxy_host: String = "", proxy_user: String = "", proxy_port: Int = 0, | 
| 96 | permissive: Boolean = false): Session = | |
| 71564 
03133befa33b
support actual_host for lrzcloud2: the proxy_host/sshd cannot resolve invented hostname (amending 1d8b6c2253e6);
 wenzelm parents: 
71562diff
changeset | 97 | init_context(options).open_session( | 
| 
03133befa33b
support actual_host for lrzcloud2: the proxy_host/sshd cannot resolve invented hostname (amending 1d8b6c2253e6);
 wenzelm parents: 
71562diff
changeset | 98 | host = host, user = user, port = port, actual_host = actual_host, | 
| 67771 | 99 | proxy_host = proxy_host, proxy_user = proxy_user, proxy_port = proxy_port, | 
| 100 | permissive = permissive) | |
| 67067 | 101 | |
| 64257 | 102 | class Context private[SSH](val options: Options, val jsch: JSch) | 
| 103 |   {
 | |
| 104 | def update_options(new_options: Options): Context = new Context(new_options, jsch) | |
| 105 | ||
| 71549 | 106 | private def connect_session(host: String, user: String = "", port: Int = 0, | 
| 67770 
25f3a278df3d
support for permissive connections, for odd situations where host keys are not accepted;
 wenzelm parents: 
67745diff
changeset | 107 | host_key_permissive: Boolean = false, | 
| 71549 | 108 | nominal_host: String = "", | 
| 109 | nominal_user: String = "", | |
| 67770 
25f3a278df3d
support for permissive connections, for odd situations where host keys are not accepted;
 wenzelm parents: 
67745diff
changeset | 110 | on_close: () => Unit = () => ()): Session = | 
| 64257 | 111 |     {
 | 
| 71383 | 112 | val session = jsch.getSession(proper_string(user).orNull, host, make_port(port)) | 
| 64257 | 113 | |
| 114 | session.setUserInfo(No_User_Info) | |
| 64325 | 115 | session.setServerAliveInterval(alive_interval(options)) | 
| 67273 
c573cfb2c407
more robust connection: prefer ServerAliveCountMax=3 (ssh default) instead of 1 (jsch default);
 wenzelm parents: 
67067diff
changeset | 116 | session.setServerAliveCountMax(alive_count_max(options)) | 
| 64257 | 117 |       session.setConfig("MaxAuthTries", "3")
 | 
| 67770 
25f3a278df3d
support for permissive connections, for odd situations where host keys are not accepted;
 wenzelm parents: 
67745diff
changeset | 118 |       if (host_key_permissive) session.setConfig("StrictHostKeyChecking", "no")
 | 
| 71549 | 119 | if (nominal_host != "") session.setHostKeyAlias(nominal_host) | 
| 64257 | 120 | |
| 121 |       if (options.bool("ssh_compression")) {
 | |
| 122 |         session.setConfig("compression.s2c", "zlib@openssh.com,zlib,none")
 | |
| 123 |         session.setConfig("compression.c2s", "zlib@openssh.com,zlib,none")
 | |
| 124 |         session.setConfig("compression_level", "9")
 | |
| 125 | } | |
| 67745 
d83efbe52438
support for proxy connection, similar to ProxyCommand in ssh config;
 wenzelm parents: 
67273diff
changeset | 126 | session.connect(connect_timeout(options)) | 
| 71549 | 127 | new Session(options, session, on_close, | 
| 128 | proper_string(nominal_host) getOrElse host, | |
| 129 | proper_string(nominal_user) getOrElse user) | |
| 67745 
d83efbe52438
support for proxy connection, similar to ProxyCommand in ssh config;
 wenzelm parents: 
67273diff
changeset | 130 | } | 
| 64257 | 131 | |
| 71564 
03133befa33b
support actual_host for lrzcloud2: the proxy_host/sshd cannot resolve invented hostname (amending 1d8b6c2253e6);
 wenzelm parents: 
71562diff
changeset | 132 | def open_session( | 
| 
03133befa33b
support actual_host for lrzcloud2: the proxy_host/sshd cannot resolve invented hostname (amending 1d8b6c2253e6);
 wenzelm parents: 
71562diff
changeset | 133 | host: String, user: String = "", port: Int = 0, actual_host: String = "", | 
| 67770 
25f3a278df3d
support for permissive connections, for odd situations where host keys are not accepted;
 wenzelm parents: 
67745diff
changeset | 134 | proxy_host: String = "", proxy_user: String = "", proxy_port: Int = 0, | 
| 
25f3a278df3d
support for permissive connections, for odd situations where host keys are not accepted;
 wenzelm parents: 
67745diff
changeset | 135 | permissive: Boolean = false): Session = | 
| 67745 
d83efbe52438
support for proxy connection, similar to ProxyCommand in ssh config;
 wenzelm parents: 
67273diff
changeset | 136 |     {
 | 
| 71564 
03133befa33b
support actual_host for lrzcloud2: the proxy_host/sshd cannot resolve invented hostname (amending 1d8b6c2253e6);
 wenzelm parents: 
71562diff
changeset | 137 | val connect_host = proper_string(actual_host) getOrElse host | 
| 
03133befa33b
support actual_host for lrzcloud2: the proxy_host/sshd cannot resolve invented hostname (amending 1d8b6c2253e6);
 wenzelm parents: 
71562diff
changeset | 138 | if (proxy_host == "") connect_session(host = connect_host, user = user, port = port) | 
| 67745 
d83efbe52438
support for proxy connection, similar to ProxyCommand in ssh config;
 wenzelm parents: 
67273diff
changeset | 139 |       else {
 | 
| 
d83efbe52438
support for proxy connection, similar to ProxyCommand in ssh config;
 wenzelm parents: 
67273diff
changeset | 140 | val proxy = connect_session(host = proxy_host, port = proxy_port, user = proxy_user) | 
| 
d83efbe52438
support for proxy connection, similar to ProxyCommand in ssh config;
 wenzelm parents: 
67273diff
changeset | 141 | |
| 
d83efbe52438
support for proxy connection, similar to ProxyCommand in ssh config;
 wenzelm parents: 
67273diff
changeset | 142 | val fw = | 
| 71564 
03133befa33b
support actual_host for lrzcloud2: the proxy_host/sshd cannot resolve invented hostname (amending 1d8b6c2253e6);
 wenzelm parents: 
71562diff
changeset | 143 |           try { proxy.port_forwarding(remote_host = connect_host, remote_port = make_port(port)) }
 | 
| 67745 
d83efbe52438
support for proxy connection, similar to ProxyCommand in ssh config;
 wenzelm parents: 
67273diff
changeset | 144 |           catch { case exn: Throwable => proxy.close; throw exn }
 | 
| 
d83efbe52438
support for proxy connection, similar to ProxyCommand in ssh config;
 wenzelm parents: 
67273diff
changeset | 145 | |
| 
d83efbe52438
support for proxy connection, similar to ProxyCommand in ssh config;
 wenzelm parents: 
67273diff
changeset | 146 |         try {
 | 
| 67770 
25f3a278df3d
support for permissive connections, for odd situations where host keys are not accepted;
 wenzelm parents: 
67745diff
changeset | 147 | connect_session(host = fw.local_host, port = fw.local_port, | 
| 71549 | 148 | host_key_permissive = permissive, | 
| 149 | nominal_host = host, nominal_user = user, user = user, | |
| 150 |             on_close = () => { fw.close; proxy.close })
 | |
| 67745 
d83efbe52438
support for proxy connection, similar to ProxyCommand in ssh config;
 wenzelm parents: 
67273diff
changeset | 151 | } | 
| 
d83efbe52438
support for proxy connection, similar to ProxyCommand in ssh config;
 wenzelm parents: 
67273diff
changeset | 152 |         catch { case exn: Throwable => fw.close; proxy.close; throw exn }
 | 
| 
d83efbe52438
support for proxy connection, similar to ProxyCommand in ssh config;
 wenzelm parents: 
67273diff
changeset | 153 | } | 
| 64257 | 154 | } | 
| 155 | } | |
| 64130 | 156 | |
| 64123 | 157 | |
| 158 | /* logging */ | |
| 159 | ||
| 160 | def logging(verbose: Boolean = true, debug: Boolean = false) | |
| 161 |   {
 | |
| 162 | JSch.setLogger(if (verbose) new Logger(debug) else null) | |
| 163 | } | |
| 164 | ||
| 165 | private class Logger(debug: Boolean) extends JSch_Logger | |
| 166 |   {
 | |
| 167 | def isEnabled(level: Int): Boolean = level != JSch_Logger.DEBUG || debug | |
| 168 | ||
| 169 | def log(level: Int, msg: String) | |
| 170 |     {
 | |
| 171 |       level match {
 | |
| 172 | case JSch_Logger.ERROR | JSch_Logger.FATAL => Output.error_message(msg) | |
| 173 | case JSch_Logger.WARN => Output.warning(msg) | |
| 174 | case _ => Output.writeln(msg) | |
| 175 | } | |
| 176 | } | |
| 177 | } | |
| 178 | ||
| 179 | ||
| 64128 | 180 | /* user info */ | 
| 181 | ||
| 182 | object No_User_Info extends UserInfo | |
| 183 |   {
 | |
| 184 | def getPassphrase: String = null | |
| 185 | def getPassword: String = null | |
| 186 | def promptPassword(msg: String): Boolean = false | |
| 187 | def promptPassphrase(msg: String): Boolean = false | |
| 188 | def promptYesNo(msg: String): Boolean = false | |
| 189 | def showMessage(msg: String): Unit = Output.writeln(msg) | |
| 190 | } | |
| 191 | ||
| 192 | ||
| 65009 | 193 | /* port forwarding */ | 
| 194 | ||
| 65010 | 195 | object Port_Forwarding | 
| 65009 | 196 |   {
 | 
| 65636 
df804cdba5f9
ssh_close for proper termination after use of database;
 wenzelm parents: 
65594diff
changeset | 197 | def open(ssh: Session, ssh_close: Boolean, | 
| 65010 | 198 | local_host: String, local_port: Int, remote_host: String, remote_port: Int): Port_Forwarding = | 
| 199 |     {
 | |
| 200 | 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 | 201 | new Port_Forwarding(ssh, ssh_close, local_host, port, remote_host, remote_port) | 
| 65010 | 202 | } | 
| 203 | } | |
| 204 | ||
| 205 | class Port_Forwarding private[SSH]( | |
| 206 | ssh: SSH.Session, | |
| 65636 
df804cdba5f9
ssh_close for proper termination after use of database;
 wenzelm parents: 
65594diff
changeset | 207 | ssh_close: Boolean, | 
| 65010 | 208 | val local_host: String, | 
| 209 | val local_port: Int, | |
| 210 | val remote_host: String, | |
| 69393 
ed0824ef337e
static type for Library.using: avoid Java 11 warnings on "Illegal reflective access";
 wenzelm parents: 
69303diff
changeset | 211 | val remote_port: Int) extends AutoCloseable | 
| 65010 | 212 |   {
 | 
| 213 | override def toString: String = | |
| 214 | local_host + ":" + local_port + ":" + remote_host + ":" + remote_port | |
| 215 | ||
| 65636 
df804cdba5f9
ssh_close for proper termination after use of database;
 wenzelm parents: 
65594diff
changeset | 216 | def close() | 
| 
df804cdba5f9
ssh_close for proper termination after use of database;
 wenzelm parents: 
65594diff
changeset | 217 |     {
 | 
| 
df804cdba5f9
ssh_close for proper termination after use of database;
 wenzelm parents: 
65594diff
changeset | 218 | ssh.session.delPortForwardingL(local_host, local_port) | 
| 
df804cdba5f9
ssh_close for proper termination after use of database;
 wenzelm parents: 
65594diff
changeset | 219 | if (ssh_close) ssh.close() | 
| 
df804cdba5f9
ssh_close for proper termination after use of database;
 wenzelm parents: 
65594diff
changeset | 220 | } | 
| 65009 | 221 | } | 
| 222 | ||
| 223 | ||
| 64191 | 224 | /* Sftp channel */ | 
| 225 | ||
| 226 | type Attrs = SftpATTRS | |
| 227 | ||
| 69302 | 228 | sealed case class Dir_Entry(name: String, is_dir: Boolean) | 
| 64191 | 229 |   {
 | 
| 69300 
8b6ab9989bcd
is_file/is_dir/read_dir: more uniform treatment of errors and boundary cases, notably for symlinks in ssh;
 wenzelm parents: 
67771diff
changeset | 230 | def is_file: Boolean = !is_dir | 
| 64191 | 231 | } | 
| 232 | ||
| 233 | ||
| 64132 | 234 | /* exec channel */ | 
| 235 | ||
| 64134 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 236 | private val exec_wait_delay = Time.seconds(0.3) | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 237 | |
| 69393 
ed0824ef337e
static type for Library.using: avoid Java 11 warnings on "Illegal reflective access";
 wenzelm parents: 
69303diff
changeset | 238 | class Exec private[SSH](session: Session, channel: ChannelExec) extends AutoCloseable | 
| 64131 | 239 |   {
 | 
| 64256 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 240 | 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 | 241 | |
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 242 |     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 | 243 | |
| 64134 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 244 | val exit_status: Future[Int] = | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 245 |       Future.thread("ssh_wait") {
 | 
| 71684 | 246 | while (!channel.isClosed) exec_wait_delay.sleep | 
| 64134 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 247 | channel.getExitStatus | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 248 | } | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 249 | |
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 250 | val stdin: OutputStream = channel.getOutputStream | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 251 | val stdout: InputStream = channel.getInputStream | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 252 | val stderr: InputStream = channel.getErrStream | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 253 | |
| 64166 | 254 | // connect after preparing streams | 
| 255 | channel.connect(connect_timeout(session.options)) | |
| 64134 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 256 | |
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 257 | def result( | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 258 | progress_stdout: String => Unit = (_: String) => (), | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 259 | progress_stderr: String => Unit = (_: String) => (), | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 260 | strict: Boolean = true): Process_Result = | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 261 |     {
 | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 262 | stdin.close | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 263 | |
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 264 | def read_lines(stream: InputStream, progress: String => Unit): List[String] = | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 265 |       {
 | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 266 | val result = new mutable.ListBuffer[String] | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 267 | val line_buffer = new ByteArrayOutputStream(100) | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 268 | def line_flush() | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 269 |         {
 | 
| 64326 | 270 | 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 | 271 | progress(line) | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 272 | result += line | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 273 | line_buffer.reset | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 274 | } | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 275 | |
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 276 | var c = 0 | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 277 | var finished = false | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 278 |         while (!finished) {
 | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 279 |           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 | 280 | if (c == 10) line_flush() | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 281 |           else if (channel.isClosed) {
 | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 282 | if (line_buffer.size > 0) line_flush() | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 283 | finished = true | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 284 | } | 
| 71684 | 285 | else exec_wait_delay.sleep | 
| 64134 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 286 | } | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 287 | |
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 288 | result.toList | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 289 | } | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 290 | |
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 291 |       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 | 292 |       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 | 293 | |
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 294 | def terminate() | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 295 |       {
 | 
| 64136 | 296 | close | 
| 64134 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 297 | out_lines.join | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 298 | err_lines.join | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 299 | exit_status.join | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 300 | } | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 301 | |
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 302 | val rc = | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 303 |         try { exit_status.join }
 | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 304 |         catch { case Exn.Interrupt() => terminate(); Exn.Interrupt.return_code }
 | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 305 | |
| 64136 | 306 | close | 
| 64134 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 307 | if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt() | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 308 | |
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 309 | Process_Result(rc, out_lines.join, err_lines.join) | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 310 | } | 
| 64131 | 311 | } | 
| 312 | ||
| 313 | ||
| 64123 | 314 | /* session */ | 
| 315 | ||
| 67745 
d83efbe52438
support for proxy connection, similar to ProxyCommand in ssh config;
 wenzelm parents: 
67273diff
changeset | 316 | class Session private[SSH]( | 
| 
d83efbe52438
support for proxy connection, similar to ProxyCommand in ssh config;
 wenzelm parents: 
67273diff
changeset | 317 | val options: Options, | 
| 
d83efbe52438
support for proxy connection, similar to ProxyCommand in ssh config;
 wenzelm parents: 
67273diff
changeset | 318 | val session: JSch_Session, | 
| 71549 | 319 | on_close: () => Unit, | 
| 320 | val nominal_host: String, | |
| 321 | val nominal_user: String) extends System with AutoCloseable | |
| 64123 | 322 |   {
 | 
| 67745 
d83efbe52438
support for proxy connection, similar to ProxyCommand in ssh config;
 wenzelm parents: 
67273diff
changeset | 323 | def update_options(new_options: Options): Session = | 
| 71549 | 324 | new Session(new_options, session, on_close, nominal_host, nominal_user) | 
| 64166 | 325 | |
| 64347 | 326 | def host: String = if (session.getHost == null) "" else session.getHost | 
| 71549 | 327 | |
| 328 | override def hg_url: String = | |
| 329 | "ssh://" + user_prefix(nominal_user) + nominal_host + "/" | |
| 66570 | 330 | |
| 64123 | 331 | override def toString: String = | 
| 71549 | 332 | user_prefix(session.getUserName) + host + port_suffix(session.getPort) + | 
| 333 | (if (session.isConnected) "" else " (disconnected)") | |
| 64123 | 334 | |
| 64256 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 335 | |
| 65009 | 336 | /* port forwarding */ | 
| 337 | ||
| 65636 
df804cdba5f9
ssh_close for proper termination after use of database;
 wenzelm parents: 
65594diff
changeset | 338 | def port_forwarding( | 
| 
df804cdba5f9
ssh_close for proper termination after use of database;
 wenzelm parents: 
65594diff
changeset | 339 | remote_port: Int, remote_host: String = "localhost", | 
| 
df804cdba5f9
ssh_close for proper termination after use of database;
 wenzelm parents: 
65594diff
changeset | 340 | local_port: Int = 0, local_host: String = "localhost", | 
| 
df804cdba5f9
ssh_close for proper termination after use of database;
 wenzelm parents: 
65594diff
changeset | 341 | ssh_close: Boolean = false): Port_Forwarding = | 
| 
df804cdba5f9
ssh_close for proper termination after use of database;
 wenzelm parents: 
65594diff
changeset | 342 | Port_Forwarding.open(this, ssh_close, local_host, local_port, remote_host, remote_port) | 
| 65009 | 343 | |
| 344 | ||
| 64256 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 345 | /* sftp channel */ | 
| 
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 |     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 | 348 | 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 | 349 | |
| 67745 
d83efbe52438
support for proxy connection, similar to ProxyCommand in ssh config;
 wenzelm parents: 
67273diff
changeset | 350 |     def close() { sftp.disconnect; session.disconnect; on_close() }
 | 
| 64256 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 351 | |
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 352 | 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 | 353 |     {
 | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 354 | 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 | 355 |       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 | 356 | } | 
| 66570 | 357 | override def expand_path(path: Path): Path = path.expand_env(settings) | 
| 64256 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 358 | def remote_path(path: Path): String = expand_path(path).implode | 
| 67066 | 359 | override def bash_path(path: Path): String = Bash.string(remote_path(path)) | 
| 64123 | 360 | |
| 64256 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 361 | 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 | 362 | 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 | 363 | 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 | 364 | 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 | 365 | 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 | 366 | |
| 69302 | 367 | private def test_entry(path: Path, as_dir: Boolean): Boolean = | 
| 368 |       try {
 | |
| 369 | val is_dir = sftp.stat(remote_path(path)).isDir | |
| 370 | if (as_dir) is_dir else !is_dir | |
| 371 | } | |
| 372 |       catch { case _: SftpException => false }
 | |
| 69300 
8b6ab9989bcd
is_file/is_dir/read_dir: more uniform treatment of errors and boundary cases, notably for symlinks in ssh;
 wenzelm parents: 
67771diff
changeset | 373 | |
| 69302 | 374 | override def is_dir(path: Path): Boolean = test_entry(path, true) | 
| 375 | override def is_file(path: Path): Boolean = test_entry(path, false) | |
| 69300 
8b6ab9989bcd
is_file/is_dir/read_dir: more uniform treatment of errors and boundary cases, notably for symlinks in ssh;
 wenzelm parents: 
67771diff
changeset | 376 | |
| 69301 | 377 | def is_link(path: Path): Boolean = | 
| 378 |       try { sftp.lstat(remote_path(path)).isLink }
 | |
| 379 |       catch { case _: SftpException => false }
 | |
| 380 | ||
| 66570 | 381 | override def mkdirs(path: Path): Unit = | 
| 64256 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 382 |       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 | 383 | execute( | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 384 |           "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 | 385 |         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 | 386 | } | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 387 | |
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 388 | def read_dir(path: Path): List[Dir_Entry] = | 
| 64191 | 389 |     {
 | 
| 69300 
8b6ab9989bcd
is_file/is_dir/read_dir: more uniform treatment of errors and boundary cases, notably for symlinks in ssh;
 wenzelm parents: 
67771diff
changeset | 390 |       if (!is_dir(path)) error("No such directory: " + path.toString)
 | 
| 
8b6ab9989bcd
is_file/is_dir/read_dir: more uniform treatment of errors and boundary cases, notably for symlinks in ssh;
 wenzelm parents: 
67771diff
changeset | 391 | |
| 
8b6ab9989bcd
is_file/is_dir/read_dir: more uniform treatment of errors and boundary cases, notably for symlinks in ssh;
 wenzelm parents: 
67771diff
changeset | 392 | val dir_name = remote_path(path) | 
| 
8b6ab9989bcd
is_file/is_dir/read_dir: more uniform treatment of errors and boundary cases, notably for symlinks in ssh;
 wenzelm parents: 
67771diff
changeset | 393 | val dir = sftp.ls(dir_name) | 
| 64256 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 394 |       (for {
 | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 395 | 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 | 396 | 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 | 397 | 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 | 398 | 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 | 399 | if name != "." && name != ".." | 
| 69302 | 400 | } | 
| 401 |       yield {
 | |
| 402 | Dir_Entry(name, | |
| 403 |           if (attrs.isLink) {
 | |
| 404 |             try { sftp.stat(dir_name + "/" + name).isDir }
 | |
| 405 |             catch { case _: SftpException => false }
 | |
| 406 | } | |
| 407 | else attrs.isDir) | |
| 69427 
ff2f39a221d4
clarified operations: uniform sorting of results;
 wenzelm parents: 
69393diff
changeset | 408 | }).toList.sortBy(_.name) | 
| 64191 | 409 | } | 
| 64135 
865dda40e1cc
provide execute operation, similar to Isabelle_System.bash;
 wenzelm parents: 
64134diff
changeset | 410 | |
| 69301 | 411 | def find_files( | 
| 412 | start: Path, | |
| 413 | pred: Path => Boolean = _ => true, | |
| 414 | include_dirs: Boolean = false, | |
| 415 | follow_links: Boolean = false): List[Path] = | |
| 64256 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 416 |     {
 | 
| 69301 | 417 | val result = new mutable.ListBuffer[Path] | 
| 418 |       def check(path: Path) { if (pred(path)) result += path }
 | |
| 419 | ||
| 420 | def find(dir: Path) | |
| 421 |       {
 | |
| 69303 | 422 | if (include_dirs) check(dir) | 
| 69301 | 423 |         if (follow_links || !is_link(dir)) {
 | 
| 424 |           for (entry <- read_dir(dir)) {
 | |
| 69302 | 425 | val path = dir + Path.basic(entry.name) | 
| 426 | if (entry.is_file) check(path) else find(path) | |
| 69301 | 427 | } | 
| 428 | } | |
| 429 | } | |
| 430 | if (is_file(start)) check(start) else find(start) | |
| 431 | ||
| 432 | result.toList | |
| 64256 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 433 | } | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 434 | |
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 435 | 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 | 436 | 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 | 437 | |
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 438 | 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 | 439 | 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 | 440 | def read_bytes(path: Path): Bytes = using(open_input(path))(Bytes.read_stream(_)) | 
| 71601 | 441 | def read(path: Path): String = using(open_input(path))(File.read_stream) | 
| 64256 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 442 | |
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 443 | 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 | 444 | 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 | 445 | def write_bytes(path: Path, bytes: Bytes): Unit = | 
| 71601 | 446 | using(open_output(path))(bytes.write_stream) | 
| 64256 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 447 | 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 | 448 | 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 | 449 | |
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 450 | |
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 451 | /* exec channel */ | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 452 | |
| 64166 | 453 | def exec(command: String): Exec = | 
| 64129 | 454 |     {
 | 
| 64256 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 455 |       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 | 456 |       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 | 457 | new Exec(this, channel) | 
| 64129 | 458 | } | 
| 64123 | 459 | |
| 66570 | 460 | override def execute(command: String, | 
| 64191 | 461 | progress_stdout: String => Unit = (_: String) => (), | 
| 462 | progress_stderr: String => Unit = (_: String) => (), | |
| 463 | strict: Boolean = true): Process_Result = | |
| 464 | exec(command).result(progress_stdout, progress_stderr, strict) | |
| 64137 | 465 | |
| 466 | ||
| 467 | /* tmp dirs */ | |
| 468 | ||
| 64306 
7b6dc1b36f20
tuned signature, in accordance to Isabelle_System;
 wenzelm parents: 
64304diff
changeset | 469 | def rm_tree(dir: Path): Unit = rm_tree(remote_path(dir)) | 
| 
7b6dc1b36f20
tuned signature, in accordance to Isabelle_System;
 wenzelm parents: 
64304diff
changeset | 470 | |
| 64137 | 471 | def rm_tree(remote_dir: String): Unit = | 
| 64304 | 472 |       execute("rm -r -f " + Bash.string(remote_dir)).check
 | 
| 64137 | 473 | |
| 474 | def tmp_dir(): String = | |
| 475 |       execute("mktemp -d -t tmp.XXXXXXXXXX").check.out
 | |
| 476 | ||
| 64233 | 477 | def with_tmp_dir[A](body: Path => A): A = | 
| 64137 | 478 |     {
 | 
| 479 | val remote_dir = tmp_dir() | |
| 64233 | 480 |       try { body(Path.explode(remote_dir)) } finally { rm_tree(remote_dir) }
 | 
| 64137 | 481 | } | 
| 64123 | 482 | } | 
| 66570 | 483 | |
| 484 | ||
| 485 | ||
| 486 | /* system operations */ | |
| 487 | ||
| 488 | trait System | |
| 489 |   {
 | |
| 490 | def hg_url: String = "" | |
| 491 | ||
| 492 | def expand_path(path: Path): Path = path.expand | |
| 67066 | 493 | def bash_path(path: Path): String = File.bash_path(path) | 
| 69300 
8b6ab9989bcd
is_file/is_dir/read_dir: more uniform treatment of errors and boundary cases, notably for symlinks in ssh;
 wenzelm parents: 
67771diff
changeset | 494 | def is_dir(path: Path): Boolean = path.is_dir | 
| 66570 | 495 | def is_file(path: Path): Boolean = path.is_file | 
| 496 | def mkdirs(path: Path): Unit = Isabelle_System.mkdirs(path) | |
| 497 | ||
| 498 | def execute(command: String, | |
| 499 | progress_stdout: String => Unit = (_: String) => (), | |
| 500 | progress_stderr: String => Unit = (_: String) => (), | |
| 501 | strict: Boolean = true): Process_Result = | |
| 502 | Isabelle_System.bash(command, progress_stdout = progress_stdout, | |
| 503 | progress_stderr = progress_stderr, strict = strict) | |
| 504 | } | |
| 505 | ||
| 506 | object Local extends System | |
| 64123 | 507 | } |