| author | wenzelm | 
| Fri, 05 May 2023 12:01:09 +0200 | |
| changeset 77967 | 6bb2f9b32804 | 
| parent 77783 | fb61887c069a | 
| child 78158 | 8b5a2e4b16d4 | 
| permissions | -rw-r--r-- | 
| 64123 | 1 | /* Title: Pure/General/ssh.scala | 
| 2 | Author: Makarius | |
| 3 | ||
| 76122 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 4 | SSH client on OpenSSH command-line tools, preferably with connection | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 5 | multiplexing, but this does not work on Windows. | 
| 64123 | 6 | */ | 
| 7 | ||
| 8 | package isabelle | |
| 9 | ||
| 10 | ||
| 73909 | 11 | import java.util.{Map => JMap}
 | 
| 76164 
5e8bc80df6b3
clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
 wenzelm parents: 
76163diff
changeset | 12 | import java.io.{File => JFile}
 | 
| 64123 | 13 | |
| 14 | ||
| 75393 | 15 | object SSH {
 | 
| 76170 | 16 | /* client command */ | 
| 17 | ||
| 18 | def client_command(port: Int = 0, control_path: String = ""): String = | |
| 19 |     if (control_path.isEmpty || control_path == Bash.string(control_path)) {
 | |
| 20 | "ssh" + | |
| 21 | (if (port > 0) " -p " + port else "") + | |
| 77369 | 22 | if_proper(control_path, " -o ControlPath=" + control_path) | 
| 76170 | 23 | } | 
| 24 |     else error ("Malformed SSH control socket: " + quote(control_path))
 | |
| 25 | ||
| 26 | ||
| 76122 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 27 | /* OpenSSH configuration and command-line */ | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 28 | |
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 29 | // see https://linux.die.net/man/5/ssh_config | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 30 |   object Config {
 | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 31 | def entry(x: String, y: String): String = x + "=" + y | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 32 | def entry(x: String, y: Int): String = entry(x, y.toString) | 
| 76165 | 33 | def entry(x: String, y: Long): String = entry(x, y.toString) | 
| 76122 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 34 | def entry(x: String, y: Boolean): String = entry(x, if (y) "yes" else "no") | 
| 64141 | 35 | |
| 76122 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 36 | def make(options: Options, | 
| 76131 
8b695e59db3f
clarified default: do not override port from ssh_config, which could be different from 22;
 wenzelm parents: 
76130diff
changeset | 37 | port: Int = 0, | 
| 76122 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 38 | user: String = "", | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 39 | control_master: Boolean = false, | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 40 | control_path: String = "" | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 41 |     ): List[String] = {
 | 
| 76168 | 42 |       val ssh_batch_mode = options.bool("ssh_batch_mode")
 | 
| 76167 | 43 |       val ssh_compression = options.bool("ssh_compression")
 | 
| 44 |       val ssh_alive_interval = options.real("ssh_alive_interval").round
 | |
| 45 |       val ssh_alive_count_max = options.int("ssh_alive_count_max")
 | |
| 46 | ||
| 76168 | 47 | List( | 
| 48 |         entry("BatchMode", ssh_batch_mode),
 | |
| 49 |         entry("Compression", ssh_compression)) :::
 | |
| 76167 | 50 |       (if (ssh_alive_interval >= 0) List(entry("ServerAliveInterval", ssh_alive_interval)) else Nil) :::
 | 
| 51 |       (if (ssh_alive_count_max >= 0) List(entry("ServerAliveCountMax", ssh_alive_count_max)) else Nil) :::
 | |
| 76131 
8b695e59db3f
clarified default: do not override port from ssh_config, which could be different from 22;
 wenzelm parents: 
76130diff
changeset | 52 |       (if (port > 0) List(entry("Port", port)) else Nil) :::
 | 
| 76122 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 53 |       (if (user.nonEmpty) List(entry("User", user)) else Nil) :::
 | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 54 |       (if (control_master) List("ControlMaster=yes", "ControlPersist=yes") else Nil) :::
 | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 55 |       (if (control_path.nonEmpty) List("ControlPath=" + control_path) else Nil)
 | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 56 | } | 
| 64325 | 57 | |
| 76147 | 58 | def option(entry: String): String = "-o " + Bash.string(entry) | 
| 59 | def option(x: String, y: String): String = option(entry(x, y)) | |
| 60 | def option(x: String, y: Int): String = option(entry(x, y)) | |
| 76165 | 61 | def option(x: String, y: Long): String = option(entry(x, y)) | 
| 76147 | 62 | def option(x: String, y: Boolean): String = option(entry(x, y)) | 
| 63 | ||
| 64 | def command(command: String, config: List[String]): String = | |
| 65 | Bash.string(command) + config.map(entry => " " + option(entry)).mkString | |
| 76122 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 66 | } | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 67 | |
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 68 |   def sftp_string(str: String): String = {
 | 
| 76150 | 69 |     val special = "[]?*\\{} \"'"
 | 
| 70 | if (str.isEmpty) "\"\"" | |
| 71 |     else if (str.exists(special.contains)) {
 | |
| 76122 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 72 | val res = new StringBuilder | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 73 |       for (c <- str) {
 | 
| 76150 | 74 | if (special.contains(c)) res += '\\' | 
| 76122 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 75 | res += c | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 76 | } | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 77 | res.toString() | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 78 | } | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 79 | else str | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 80 | } | 
| 67273 
c573cfb2c407
more robust connection: prefer ServerAliveCountMax=3 (ssh default) instead of 1 (jsch default);
 wenzelm parents: 
67067diff
changeset | 81 | |
| 64123 | 82 | |
| 76115 
f17393e21388
clarified signature: discontinue somewhat pointless SSH.Context;
 wenzelm parents: 
76100diff
changeset | 83 | /* open session */ | 
| 
f17393e21388
clarified signature: discontinue somewhat pointless SSH.Context;
 wenzelm parents: 
76100diff
changeset | 84 | |
| 
f17393e21388
clarified signature: discontinue somewhat pointless SSH.Context;
 wenzelm parents: 
76100diff
changeset | 85 | def open_session( | 
| 
f17393e21388
clarified signature: discontinue somewhat pointless SSH.Context;
 wenzelm parents: 
76100diff
changeset | 86 | options: Options, | 
| 
f17393e21388
clarified signature: discontinue somewhat pointless SSH.Context;
 wenzelm parents: 
76100diff
changeset | 87 | host: String, | 
| 76122 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 88 | port: Int = 0, | 
| 76148 
769ebb139a32
support port forwarding without multiplexing (for the sake of Windows);
 wenzelm parents: 
76147diff
changeset | 89 | user: String = "" | 
| 76115 
f17393e21388
clarified signature: discontinue somewhat pointless SSH.Context;
 wenzelm parents: 
76100diff
changeset | 90 |   ): Session = {
 | 
| 76148 
769ebb139a32
support port forwarding without multiplexing (for the sake of Windows);
 wenzelm parents: 
76147diff
changeset | 91 |     val multiplex = options.bool("ssh_multiplexing") && !Platform.is_windows
 | 
| 76122 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 92 | val (control_master, control_path) = | 
| 76161 | 93 |       if (multiplex) (true, Isabelle_System.tmp_file("ssh", initialized = false).getPath)
 | 
| 76122 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 94 | else (false, "") | 
| 76131 
8b695e59db3f
clarified default: do not override port from ssh_config, which could be different from 22;
 wenzelm parents: 
76130diff
changeset | 95 | new Session(options, host, port, user, control_master, control_path) | 
| 64257 | 96 | } | 
| 64130 | 97 | |
| 76122 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 98 | class Session private[SSH]( | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 99 | val options: Options, | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 100 | val host: String, | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 101 | val port: Int, | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 102 | val user: String, | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 103 | control_master: Boolean, | 
| 76136 
1bb677cceea4
let rsync re-use ssh connection via control path;
 wenzelm parents: 
76133diff
changeset | 104 | val control_path: String | 
| 76122 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 105 |   ) extends System {
 | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 106 | ssh => | 
| 64128 | 107 | |
| 77782 
127d077cccfe
clarified signature: avoid object-oriented "dispatch";
 wenzelm parents: 
77761diff
changeset | 108 | override def is_local: Boolean = false | 
| 
127d077cccfe
clarified signature: avoid object-oriented "dispatch";
 wenzelm parents: 
77761diff
changeset | 109 | |
| 76133 | 110 | def port_suffix: String = if (port > 0) ":" + port else "" | 
| 111 | def user_prefix: String = if (user.nonEmpty) user + "@" else "" | |
| 112 | ||
| 113 | override def toString: String = user_prefix + host + port_suffix | |
| 77761 | 114 | override def print: String = " (ssh " + toString + ")" | 
| 76132 | 115 | override def hg_url: String = "ssh://" + toString + "/" | 
| 77783 
fb61887c069a
clarified underlying SSH session of "isabelle hg_sync" and "isabelle sync";
 wenzelm parents: 
77782diff
changeset | 116 | override def client_command: String = | 
| 
fb61887c069a
clarified underlying SSH session of "isabelle hg_sync" and "isabelle sync";
 wenzelm parents: 
77782diff
changeset | 117 | SSH.client_command(port = port, control_path = control_path) | 
| 76133 | 118 | override def rsync_prefix: String = user_prefix + host + ":" | 
| 64191 | 119 | |
| 120 | ||
| 76147 | 121 | /* local ssh commands */ | 
| 64256 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 122 | |
| 76122 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 123 | def run_command(command: String, | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 124 | master: Boolean = false, | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 125 | opts: String = "", | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 126 | args: String = "", | 
| 76164 
5e8bc80df6b3
clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
 wenzelm parents: 
76163diff
changeset | 127 | cwd: JFile = null, | 
| 77092 | 128 | redirect: Boolean = false, | 
| 64134 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 129 | progress_stdout: String => Unit = (_: String) => (), | 
| 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 130 | progress_stderr: String => Unit = (_: String) => (), | 
| 75393 | 131 | strict: Boolean = true | 
| 132 |     ): Process_Result = {
 | |
| 76122 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 133 | val config = | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 134 | Config.make(options, port = port, user = user, | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 135 | control_master = master, control_path = control_path) | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 136 | val cmd = | 
| 76147 | 137 | Config.command(command, config) + | 
| 77369 | 138 | if_proper(opts, " " + opts) + | 
| 139 | if_proper(args, " -- " + args) | |
| 77092 | 140 | Isabelle_System.bash(cmd, cwd = cwd, | 
| 141 | redirect = redirect, | |
| 142 | progress_stdout = progress_stdout, | |
| 143 | progress_stderr = progress_stderr, | |
| 144 | strict = strict) | |
| 76122 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 145 | } | 
| 64134 
57581e4026fe
proper support for exec channel (see also bash.scala);
 wenzelm parents: 
64133diff
changeset | 146 | |
| 76164 
5e8bc80df6b3
clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
 wenzelm parents: 
76163diff
changeset | 147 | def run_sftp( | 
| 
5e8bc80df6b3
clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
 wenzelm parents: 
76163diff
changeset | 148 | script: String, | 
| 
5e8bc80df6b3
clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
 wenzelm parents: 
76163diff
changeset | 149 | init: Path => Unit = _ => (), | 
| 
5e8bc80df6b3
clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
 wenzelm parents: 
76163diff
changeset | 150 | exit: Path => Unit = _ => () | 
| 
5e8bc80df6b3
clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
 wenzelm parents: 
76163diff
changeset | 151 |     ): Process_Result = {
 | 
| 
5e8bc80df6b3
clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
 wenzelm parents: 
76163diff
changeset | 152 |       Isabelle_System.with_tmp_dir("ssh") { dir =>
 | 
| 
5e8bc80df6b3
clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
 wenzelm parents: 
76163diff
changeset | 153 | init(dir) | 
| 
5e8bc80df6b3
clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
 wenzelm parents: 
76163diff
changeset | 154 |         File.write(dir + Path.explode("script"), script)
 | 
| 
5e8bc80df6b3
clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
 wenzelm parents: 
76163diff
changeset | 155 | val result = | 
| 
5e8bc80df6b3
clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
 wenzelm parents: 
76163diff
changeset | 156 |           run_command("sftp", opts = "-b script", args = Bash.string(host), cwd = dir.file).check
 | 
| 
5e8bc80df6b3
clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
 wenzelm parents: 
76163diff
changeset | 157 | exit(dir) | 
| 
5e8bc80df6b3
clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
 wenzelm parents: 
76163diff
changeset | 158 | result | 
| 76116 
c4dc343fdbcb
clarified signature: avoid exposure of JSch types;
 wenzelm parents: 
76115diff
changeset | 159 | } | 
| 
c4dc343fdbcb
clarified signature: avoid exposure of JSch types;
 wenzelm parents: 
76115diff
changeset | 160 | } | 
| 65009 | 161 | |
| 76122 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 162 |     def run_ssh(master: Boolean = false, opts: String = "", args: String = ""): Process_Result = {
 | 
| 77369 | 163 | val args1 = Bash.string(host) + if_proper(args, " " + args) | 
| 76122 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 164 |       run_command("ssh", master = master, opts = opts, args = args1)
 | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 165 | } | 
| 64256 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 166 | |
| 76122 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 167 | |
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 168 | /* init and exit */ | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 169 | |
| 76151 | 170 |     val user_home: String = {
 | 
| 76154 
dfddb80fc515
more robust: do not assume Bash syntax while testing for it;
 wenzelm parents: 
76151diff
changeset | 171 | run_ssh(master = control_master, args = "printenv HOME \";\" printenv SHELL").check.out_lines | 
| 
dfddb80fc515
more robust: do not assume Bash syntax while testing for it;
 wenzelm parents: 
76151diff
changeset | 172 |       match {
 | 
| 76149 
ccc748255342
more robust: Bash.string operations require remote bash;
 wenzelm parents: 
76148diff
changeset | 173 | case List(user_home, shell) => | 
| 
ccc748255342
more robust: Bash.string operations require remote bash;
 wenzelm parents: 
76148diff
changeset | 174 |           if (shell.endsWith("/bash")) user_home
 | 
| 
ccc748255342
more robust: Bash.string operations require remote bash;
 wenzelm parents: 
76148diff
changeset | 175 |           else {
 | 
| 
ccc748255342
more robust: Bash.string operations require remote bash;
 wenzelm parents: 
76148diff
changeset | 176 |             error("Bad SHELL for " + quote(toString) + " -- expected GNU bash, but found " + shell)
 | 
| 
ccc748255342
more robust: Bash.string operations require remote bash;
 wenzelm parents: 
76148diff
changeset | 177 | } | 
| 
ccc748255342
more robust: Bash.string operations require remote bash;
 wenzelm parents: 
76148diff
changeset | 178 |         case _ => error("Malformed remote environment for " + quote(toString))
 | 
| 
ccc748255342
more robust: Bash.string operations require remote bash;
 wenzelm parents: 
76148diff
changeset | 179 | } | 
| 76151 | 180 | } | 
| 76122 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 181 | |
| 77079 
395a0701a125
clarified signature: minimal interface for getenv/expand_env, instead of bulky java.util.Map;
 wenzelm parents: 
77077diff
changeset | 182 | val settings: Isabelle_System.Settings = | 
| 
395a0701a125
clarified signature: minimal interface for getenv/expand_env, instead of bulky java.util.Map;
 wenzelm parents: 
77077diff
changeset | 183 | (name: String) => if (name == "HOME" || name == "USER_HOME") user_home else "" | 
| 64256 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 184 | |
| 76122 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 185 |     override def close(): Unit = {
 | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 186 | if (control_path.nonEmpty) run_ssh(opts = "-O exit").check | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 187 | } | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 188 | |
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 189 | |
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 190 | /* remote commands */ | 
| 64256 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 191 | |
| 76122 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 192 | override def execute(cmd_line: String, | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 193 | progress_stdout: String => Unit = (_: String) => (), | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 194 | progress_stderr: String => Unit = (_: String) => (), | 
| 77092 | 195 | redirect: Boolean = false, | 
| 76122 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 196 | settings: Boolean = true, | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 197 | strict: Boolean = true | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 198 |     ): Process_Result = {
 | 
| 77077 
c2e8ba15a10a
discontinued adhoc change of environment (from c62b99e3ec07), which has been mostly superseded by expand_path / remote_path (from ef6f7e8a018c);
 wenzelm parents: 
77076diff
changeset | 199 |       run_command("ssh",
 | 
| 
c2e8ba15a10a
discontinued adhoc change of environment (from c62b99e3ec07), which has been mostly superseded by expand_path / remote_path (from ef6f7e8a018c);
 wenzelm parents: 
77076diff
changeset | 200 | args = Bash.string(host) + " " + Bash.string(cmd_line), | 
| 
c2e8ba15a10a
discontinued adhoc change of environment (from c62b99e3ec07), which has been mostly superseded by expand_path / remote_path (from ef6f7e8a018c);
 wenzelm parents: 
77076diff
changeset | 201 | progress_stdout = progress_stdout, | 
| 
c2e8ba15a10a
discontinued adhoc change of environment (from c62b99e3ec07), which has been mostly superseded by expand_path / remote_path (from ef6f7e8a018c);
 wenzelm parents: 
77076diff
changeset | 202 | progress_stderr = progress_stderr, | 
| 77092 | 203 | redirect = redirect, | 
| 77077 
c2e8ba15a10a
discontinued adhoc change of environment (from c62b99e3ec07), which has been mostly superseded by expand_path / remote_path (from ef6f7e8a018c);
 wenzelm parents: 
77076diff
changeset | 204 | strict = strict) | 
| 64256 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 205 | } | 
| 76122 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 206 | |
| 77054 | 207 | override def download_file( | 
| 208 | url_name: String, | |
| 209 | file: Path, | |
| 210 | progress: Progress = new Progress | |
| 211 |     ): Unit = {
 | |
| 212 | val cmd_line = | |
| 213 |         File.read(Path.explode("~~/lib/scripts/download_file")) + "\n" +
 | |
| 214 | "download_file " + Bash.string(url_name) + " " + bash_path(file) | |
| 215 | execute(cmd_line, | |
| 77509 
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
 wenzelm parents: 
77369diff
changeset | 216 | progress_stdout = progress.echo(_), | 
| 
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
 wenzelm parents: 
77369diff
changeset | 217 | progress_stderr = progress.echo(_)).check | 
| 77054 | 218 | } | 
| 219 | ||
| 76122 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 220 | override lazy val isabelle_platform: Isabelle_Platform = Isabelle_Platform(ssh = Some(ssh)) | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 221 | |
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 222 | |
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 223 | /* remote file-system */ | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 224 | |
| 66570 | 225 | override def expand_path(path: Path): Path = path.expand_env(settings) | 
| 77076 | 226 |     override def absolute_path(path: Path): Path = {
 | 
| 227 | val path1 = expand_path(path) | |
| 228 | if (path1.is_absolute) path1 else Path.explode(user_home) + path1 | |
| 229 | } | |
| 230 | ||
| 64256 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 231 | def remote_path(path: Path): String = expand_path(path).implode | 
| 76122 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 232 | |
| 67066 | 233 | override def bash_path(path: Path): String = Bash.string(remote_path(path)) | 
| 76122 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 234 | def sftp_path(path: Path): String = sftp_string(remote_path(path)) | 
| 64256 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 235 | |
| 76122 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 236 | override def is_dir(path: Path): Boolean = run_ssh(args = "test -d " + bash_path(path)).ok | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 237 | override def is_file(path: Path): Boolean = run_ssh(args = "test -f " + bash_path(path)).ok | 
| 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 | 238 | |
| 77092 | 239 |     override def delete(path: Path): Unit = {
 | 
| 240 | val cmd = if (is_dir(path)) "rmdir" else if (is_file(path)) "rm" else "" | |
| 241 | if (cmd.nonEmpty) run_sftp(cmd + " " + sftp_path(path)) | |
| 242 | } | |
| 243 | ||
| 244 | override def set_executable(path: Path, flag: Boolean): Unit = | |
| 245 |       if (!execute("chmod a" + (if (flag) "+" else "-") + "x " + bash_path(path)).ok) {
 | |
| 246 |         error("Failed to change executable status of " + quote(remote_path(path)))
 | |
| 247 | } | |
| 248 | ||
| 75393 | 249 |     override def make_directory(path: Path): Path = {
 | 
| 76122 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 250 |       if (!execute("mkdir -p " + bash_path(path)).ok) {
 | 
| 76118 | 251 |         error("Failed to create directory: " + quote(remote_path(path)))
 | 
| 64256 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 252 | } | 
| 72376 | 253 | path | 
| 254 | } | |
| 64256 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 255 | |
| 77059 | 256 |     override def copy_file(src: Path, dst: Path): Unit = {
 | 
| 257 | val direct = if (is_dir(dst)) "/." else "" | |
| 258 |       if (!execute("cp -a " + bash_path(src) + " " + bash_path(dst) + direct).ok) {
 | |
| 259 |         error("Failed to copy file " + expand_path(src) + " to " +
 | |
| 260 | expand_path(dst) + " (ssh " + toString + ")") | |
| 261 | } | |
| 262 | } | |
| 263 | ||
| 77096 | 264 | override def read_dir(path: Path): List[String] = | 
| 76241 | 265 |       run_sftp("@cd " + sftp_path(path) + "\n@ls -1 -a").out_lines.flatMap(s =>
 | 
| 266 | if (s == "." || s == "..") None | |
| 76122 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 267 |         else Some(Library.perhaps_unprefix("./", s)))
 | 
| 64256 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 268 | |
| 76164 
5e8bc80df6b3
clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
 wenzelm parents: 
76163diff
changeset | 269 |     private def get_file[A](path: Path, f: Path => A): A = {
 | 
| 
5e8bc80df6b3
clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
 wenzelm parents: 
76163diff
changeset | 270 | var result: Option[A] = None | 
| 
5e8bc80df6b3
clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
 wenzelm parents: 
76163diff
changeset | 271 |       run_sftp("get -p " + sftp_path(path) + " local",
 | 
| 
5e8bc80df6b3
clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
 wenzelm parents: 
76163diff
changeset | 272 |         exit = dir => result = Some(f(dir + Path.explode("local"))))
 | 
| 
5e8bc80df6b3
clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
 wenzelm parents: 
76163diff
changeset | 273 | result.get | 
| 
5e8bc80df6b3
clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
 wenzelm parents: 
76163diff
changeset | 274 | } | 
| 
5e8bc80df6b3
clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
 wenzelm parents: 
76163diff
changeset | 275 | |
| 
5e8bc80df6b3
clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
 wenzelm parents: 
76163diff
changeset | 276 | private def put_file(path: Path, f: Path => Unit): Unit = | 
| 
5e8bc80df6b3
clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
 wenzelm parents: 
76163diff
changeset | 277 |       run_sftp("put -p local " + sftp_path(path),
 | 
| 
5e8bc80df6b3
clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
 wenzelm parents: 
76163diff
changeset | 278 |         init = dir => f(dir + Path.explode("local")))
 | 
| 
5e8bc80df6b3
clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
 wenzelm parents: 
76163diff
changeset | 279 | |
| 73634 | 280 | override def read_file(path: Path, local_path: Path): Unit = | 
| 76164 
5e8bc80df6b3
clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
 wenzelm parents: 
76163diff
changeset | 281 | get_file(path, Isabelle_System.copy_file(_, local_path)) | 
| 76122 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 282 | override def read_bytes(path: Path): Bytes = | 
| 76164 
5e8bc80df6b3
clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
 wenzelm parents: 
76163diff
changeset | 283 | get_file(path, Bytes.read) | 
| 
5e8bc80df6b3
clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
 wenzelm parents: 
76163diff
changeset | 284 | override def read(path: Path): String = | 
| 
5e8bc80df6b3
clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
 wenzelm parents: 
76163diff
changeset | 285 | get_file(path, File.read) | 
| 64256 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64254diff
changeset | 286 | |
| 73634 | 287 | override def write_file(path: Path, local_path: Path): Unit = | 
| 76164 
5e8bc80df6b3
clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
 wenzelm parents: 
76163diff
changeset | 288 | put_file(path, Isabelle_System.copy_file(local_path, _)) | 
| 77092 | 289 | override def write_bytes(path: Path, bytes: Bytes): Unit = | 
| 76164 
5e8bc80df6b3
clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
 wenzelm parents: 
76163diff
changeset | 290 | put_file(path, Bytes.write(_, bytes)) | 
| 77092 | 291 | override def write(path: Path, text: String): Unit = | 
| 76164 
5e8bc80df6b3
clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
 wenzelm parents: 
76163diff
changeset | 292 | put_file(path, File.write(_, text)) | 
| 72338 | 293 | |
| 64137 | 294 | |
| 295 | /* tmp dirs */ | |
| 296 | ||
| 77092 | 297 | override def rm_tree(dir: Path): Unit = rm_tree(remote_path(dir)) | 
| 64306 
7b6dc1b36f20
tuned signature, in accordance to Isabelle_System;
 wenzelm parents: 
64304diff
changeset | 298 | |
| 64137 | 299 | def rm_tree(remote_dir: String): Unit = | 
| 64304 | 300 |       execute("rm -r -f " + Bash.string(remote_dir)).check
 | 
| 64137 | 301 | |
| 302 | def tmp_dir(): String = | |
| 76163 
9df6f51ebf45
more robust, notably for macOS (see also ff92d6edff2c);
 wenzelm parents: 
76161diff
changeset | 303 |       execute("mktemp -d /tmp/ssh-XXXXXXXXXXXX").check.out
 | 
| 64137 | 304 | |
| 75393 | 305 |     override def with_tmp_dir[A](body: Path => A): A = {
 | 
| 64137 | 306 | val remote_dir = tmp_dir() | 
| 76122 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 307 |       try { body(Path.explode(remote_dir)) }
 | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 308 |       finally { rm_tree(remote_dir) }
 | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 309 | } | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 310 | |
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 311 | |
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 312 | /* port forwarding */ | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 313 | |
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 314 | def port_forwarding( | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 315 | remote_port: Int, | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 316 | remote_host: String = "localhost", | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 317 | local_port: Int = 0, | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 318 | local_host: String = "localhost", | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 319 | ssh_close: Boolean = false | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 320 |     ): Port_Forwarding = {
 | 
| 76145 | 321 | val port = if (local_port > 0) local_port else Isabelle_System.local_port() | 
| 322 | ||
| 76147 | 323 |       val forward = List(local_host, port, remote_host, remote_port).mkString(":")
 | 
| 324 | val forward_option = "-L " + Bash.string(forward) | |
| 325 | ||
| 326 | val cancel: () => Unit = | |
| 327 |         if (control_path.nonEmpty) {
 | |
| 328 | run_ssh(opts = forward_option + " -O forward").check | |
| 329 | () => run_ssh(opts = forward_option + " -O cancel") // permissive | |
| 330 | } | |
| 76148 
769ebb139a32
support port forwarding without multiplexing (for the sake of Windows);
 wenzelm parents: 
76147diff
changeset | 331 |         else {
 | 
| 
769ebb139a32
support port forwarding without multiplexing (for the sake of Windows);
 wenzelm parents: 
76147diff
changeset | 332 | val result = Synchronized[Exn.Result[Boolean]](Exn.Res(false)) | 
| 
769ebb139a32
support port forwarding without multiplexing (for the sake of Windows);
 wenzelm parents: 
76147diff
changeset | 333 |           val thread = Isabelle_Thread.fork("port_forwarding") {
 | 
| 
769ebb139a32
support port forwarding without multiplexing (for the sake of Windows);
 wenzelm parents: 
76147diff
changeset | 334 | val opts = | 
| 
769ebb139a32
support port forwarding without multiplexing (for the sake of Windows);
 wenzelm parents: 
76147diff
changeset | 335 | forward_option + | 
| 
769ebb139a32
support port forwarding without multiplexing (for the sake of Windows);
 wenzelm parents: 
76147diff
changeset | 336 |                 " " + Config.option("SessionType", "none") +
 | 
| 
769ebb139a32
support port forwarding without multiplexing (for the sake of Windows);
 wenzelm parents: 
76147diff
changeset | 337 |                 " " + Config.option("PermitLocalCommand", true) +
 | 
| 
769ebb139a32
support port forwarding without multiplexing (for the sake of Windows);
 wenzelm parents: 
76147diff
changeset | 338 |                 " " + Config.option("LocalCommand", "pwd")
 | 
| 
769ebb139a32
support port forwarding without multiplexing (for the sake of Windows);
 wenzelm parents: 
76147diff
changeset | 339 |             try {
 | 
| 
769ebb139a32
support port forwarding without multiplexing (for the sake of Windows);
 wenzelm parents: 
76147diff
changeset | 340 |               run_command("ssh", opts = opts, args = Bash.string(host),
 | 
| 
769ebb139a32
support port forwarding without multiplexing (for the sake of Windows);
 wenzelm parents: 
76147diff
changeset | 341 | progress_stdout = _ => result.change(_ => Exn.Res(true))).check | 
| 
769ebb139a32
support port forwarding without multiplexing (for the sake of Windows);
 wenzelm parents: 
76147diff
changeset | 342 | } | 
| 
769ebb139a32
support port forwarding without multiplexing (for the sake of Windows);
 wenzelm parents: 
76147diff
changeset | 343 |             catch { case exn: Throwable => result.change(_ => Exn.Exn(exn)) }
 | 
| 
769ebb139a32
support port forwarding without multiplexing (for the sake of Windows);
 wenzelm parents: 
76147diff
changeset | 344 | } | 
| 
769ebb139a32
support port forwarding without multiplexing (for the sake of Windows);
 wenzelm parents: 
76147diff
changeset | 345 |           result.guarded_access {
 | 
| 
769ebb139a32
support port forwarding without multiplexing (for the sake of Windows);
 wenzelm parents: 
76147diff
changeset | 346 | case res@Exn.Res(ok) => if (ok) Some((), res) else None | 
| 
769ebb139a32
support port forwarding without multiplexing (for the sake of Windows);
 wenzelm parents: 
76147diff
changeset | 347 | case Exn.Exn(exn) => throw exn | 
| 
769ebb139a32
support port forwarding without multiplexing (for the sake of Windows);
 wenzelm parents: 
76147diff
changeset | 348 | } | 
| 
769ebb139a32
support port forwarding without multiplexing (for the sake of Windows);
 wenzelm parents: 
76147diff
changeset | 349 | () => thread.interrupt() | 
| 
769ebb139a32
support port forwarding without multiplexing (for the sake of Windows);
 wenzelm parents: 
76147diff
changeset | 350 | } | 
| 76147 | 351 | |
| 352 | val shutdown_hook = | |
| 353 |         Isabelle_System.create_shutdown_hook { cancel() }
 | |
| 76122 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 354 | |
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 355 |       new Port_Forwarding(host, port, remote_host, remote_port) {
 | 
| 76147 | 356 | override def toString: String = forward | 
| 76122 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 357 |         override def close(): Unit = {
 | 
| 76147 | 358 | cancel() | 
| 359 | Isabelle_System.remove_shutdown_hook(shutdown_hook) | |
| 76122 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 360 | if (ssh_close) ssh.close() | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 361 | } | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 362 | } | 
| 64137 | 363 | } | 
| 64123 | 364 | } | 
| 66570 | 365 | |
| 76116 
c4dc343fdbcb
clarified signature: avoid exposure of JSch types;
 wenzelm parents: 
76115diff
changeset | 366 | abstract class Port_Forwarding private[SSH]( | 
| 76122 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 367 | val host: String, | 
| 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 368 | val port: Int, | 
| 76116 
c4dc343fdbcb
clarified signature: avoid exposure of JSch types;
 wenzelm parents: 
76115diff
changeset | 369 | val remote_host: String, | 
| 
c4dc343fdbcb
clarified signature: avoid exposure of JSch types;
 wenzelm parents: 
76115diff
changeset | 370 | val remote_port: Int | 
| 76122 
b8f26c20d3b1
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
 wenzelm parents: 
76119diff
changeset | 371 | ) extends AutoCloseable | 
| 76116 
c4dc343fdbcb
clarified signature: avoid exposure of JSch types;
 wenzelm parents: 
76115diff
changeset | 372 | |
| 66570 | 373 | |
| 374 | /* system operations */ | |
| 375 | ||
| 77783 
fb61887c069a
clarified underlying SSH session of "isabelle hg_sync" and "isabelle sync";
 wenzelm parents: 
77782diff
changeset | 376 | def open_system( | 
| 
fb61887c069a
clarified underlying SSH session of "isabelle hg_sync" and "isabelle sync";
 wenzelm parents: 
77782diff
changeset | 377 | options: Options, | 
| 
fb61887c069a
clarified underlying SSH session of "isabelle hg_sync" and "isabelle sync";
 wenzelm parents: 
77782diff
changeset | 378 | host: String, | 
| 
fb61887c069a
clarified underlying SSH session of "isabelle hg_sync" and "isabelle sync";
 wenzelm parents: 
77782diff
changeset | 379 | port: Int = 0, | 
| 
fb61887c069a
clarified underlying SSH session of "isabelle hg_sync" and "isabelle sync";
 wenzelm parents: 
77782diff
changeset | 380 | user: String = "" | 
| 
fb61887c069a
clarified underlying SSH session of "isabelle hg_sync" and "isabelle sync";
 wenzelm parents: 
77782diff
changeset | 381 |   ): System = {
 | 
| 
fb61887c069a
clarified underlying SSH session of "isabelle hg_sync" and "isabelle sync";
 wenzelm parents: 
77782diff
changeset | 382 | if (host.isEmpty) Local | 
| 
fb61887c069a
clarified underlying SSH session of "isabelle hg_sync" and "isabelle sync";
 wenzelm parents: 
77782diff
changeset | 383 | else open_session(options, host = host, port = port, user = user) | 
| 
fb61887c069a
clarified underlying SSH session of "isabelle hg_sync" and "isabelle sync";
 wenzelm parents: 
77782diff
changeset | 384 | } | 
| 
fb61887c069a
clarified underlying SSH session of "isabelle hg_sync" and "isabelle sync";
 wenzelm parents: 
77782diff
changeset | 385 | |
| 75393 | 386 |   trait System extends AutoCloseable {
 | 
| 77782 
127d077cccfe
clarified signature: avoid object-oriented "dispatch";
 wenzelm parents: 
77761diff
changeset | 387 | def is_local: Boolean | 
| 
127d077cccfe
clarified signature: avoid object-oriented "dispatch";
 wenzelm parents: 
77761diff
changeset | 388 | |
| 73634 | 389 | def close(): Unit = () | 
| 390 | ||
| 77761 | 391 | override def toString: String = "SSH.Local" | 
| 392 | def print: String = "" | |
| 66570 | 393 | def hg_url: String = "" | 
| 77783 
fb61887c069a
clarified underlying SSH session of "isabelle hg_sync" and "isabelle sync";
 wenzelm parents: 
77782diff
changeset | 394 | def client_command: String = "" | 
| 66570 | 395 | |
| 75500 | 396 | def rsync_prefix: String = "" | 
| 75517 | 397 | def rsync_path(path: Path): String = rsync_prefix + expand_path(path).implode | 
| 75500 | 398 | |
| 66570 | 399 | def expand_path(path: Path): Path = path.expand | 
| 77076 | 400 | def absolute_path(path: Path): Path = path.absolute | 
| 67066 | 401 | 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 | 402 | def is_dir(path: Path): Boolean = path.is_dir | 
| 66570 | 403 | def is_file(path: Path): Boolean = path.is_file | 
| 77092 | 404 | def delete(path: Path): Unit = path.file.delete | 
| 405 | def set_executable(path: Path, flag: Boolean): Unit = File.set_executable(path, flag) | |
| 72376 | 406 | def make_directory(path: Path): Path = Isabelle_System.make_directory(path) | 
| 77092 | 407 | def rm_tree(dir: Path): Unit = Isabelle_System.rm_tree(dir) | 
| 73634 | 408 |     def with_tmp_dir[A](body: Path => A): A = Isabelle_System.with_tmp_dir("tmp")(body)
 | 
| 77096 | 409 | def read_dir(path: Path): List[String] = File.read_dir(path) | 
| 77059 | 410 | def copy_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path1, path2) | 
| 73634 | 411 | def read_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path1, path2) | 
| 75513 | 412 | def read_bytes(path: Path): Bytes = Bytes.read(path) | 
| 413 | def read(path: Path): String = File.read(path) | |
| 77092 | 414 | def write_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path2, path1) | 
| 415 | def write_bytes(path: Path, bytes: Bytes): Unit = Bytes.write(path, bytes) | |
| 416 | def write(path: Path, text: String): Unit = File.write(path, text) | |
| 66570 | 417 | |
| 418 | def execute(command: String, | |
| 419 | progress_stdout: String => Unit = (_: String) => (), | |
| 420 | progress_stderr: String => Unit = (_: String) => (), | |
| 77092 | 421 | redirect: Boolean = false, | 
| 73634 | 422 | settings: Boolean = true, | 
| 66570 | 423 | strict: Boolean = true): Process_Result = | 
| 73634 | 424 | Isabelle_System.bash(command, | 
| 425 | progress_stdout = progress_stdout, | |
| 426 | progress_stderr = progress_stderr, | |
| 77092 | 427 | redirect = redirect, | 
| 73634 | 428 | env = if (settings) Isabelle_System.settings() else null, | 
| 429 | strict = strict) | |
| 72338 | 430 | |
| 77760 | 431 | def new_directory(path: Path): Path = | 
| 432 |       if (is_dir(path)) error("Directory already exists: " + absolute_path(path))
 | |
| 433 | else make_directory(path) | |
| 434 | ||
| 77054 | 435 | def download_file(url_name: String, file: Path, progress: Progress = new Progress): Unit = | 
| 436 | Isabelle_System.download_file(url_name, file, progress = progress) | |
| 437 | ||
| 72340 | 438 | def isabelle_platform: Isabelle_Platform = Isabelle_Platform() | 
| 77130 | 439 | |
| 440 | def isabelle_platform_family: Platform.Family.Value = | |
| 441 | Platform.Family.parse(isabelle_platform.ISABELLE_PLATFORM_FAMILY) | |
| 66570 | 442 | } | 
| 443 | ||
| 77782 
127d077cccfe
clarified signature: avoid object-oriented "dispatch";
 wenzelm parents: 
77761diff
changeset | 444 |   object Local extends System {
 | 
| 
127d077cccfe
clarified signature: avoid object-oriented "dispatch";
 wenzelm parents: 
77761diff
changeset | 445 | override def is_local: Boolean = true | 
| 
127d077cccfe
clarified signature: avoid object-oriented "dispatch";
 wenzelm parents: 
77761diff
changeset | 446 | } | 
| 64123 | 447 | } |