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