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