src/Pure/General/ssh.scala
author wenzelm
Sun, 11 Sep 2022 23:27:20 +0200
changeset 76116 c4dc343fdbcb
parent 76115 f17393e21388
child 76117 531248fd8952
permissions -rw-r--r--
clarified signature: avoid exposure of JSch types;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/General/ssh.scala
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
     3
64124
818265654e60 tuned comment;
wenzelm
parents: 64123
diff changeset
     4
SSH client based on JSch (see also http://www.jcraft.com/jsch/examples).
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
     5
*/
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
     6
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
     7
package isabelle
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
     8
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
     9
73909
1d0d9772fff0 tuned imports;
wenzelm
parents: 73897
diff changeset
    10
import java.util.{Map => JMap}
64134
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
    11
import java.io.{InputStream, OutputStream, ByteArrayOutputStream}
64131
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
    12
71358
ec48da635e6c unused;
wenzelm
parents: 71307
diff changeset
    13
import scala.collection.mutable
71601
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71564
diff changeset
    14
import scala.util.matching.Regex
64131
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
    15
64222
184e3a932778 clarified signature;
wenzelm
parents: 64191
diff changeset
    16
import com.jcraft.jsch.{JSch, Logger => JSch_Logger, Session => JSch_Session, SftpException,
75548
wenzelm
parents: 75547
diff changeset
    17
  OpenSSHConfig, UserInfo, ChannelExec, ChannelSftp, SftpATTRS, JSchException}
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    18
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    19
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74306
diff changeset
    20
object SSH {
64185
wenzelm
parents: 64166
diff changeset
    21
  /* target machine: user@host syntax */
64141
79cd4be708fb support user@host syntax;
wenzelm
parents: 64137
diff changeset
    22
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74306
diff changeset
    23
  object Target {
71601
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71564
diff changeset
    24
    val User_Host: Regex = "^([^@]+)@(.+)$".r
64141
79cd4be708fb support user@host syntax;
wenzelm
parents: 64137
diff changeset
    25
79cd4be708fb support user@host syntax;
wenzelm
parents: 64137
diff changeset
    26
    def parse(s: String): (String, String) =
79cd4be708fb support user@host syntax;
wenzelm
parents: 64137
diff changeset
    27
      s match {
71307
wenzelm
parents: 69427
diff changeset
    28
        case User_Host(user, host) => (user, host)
64141
79cd4be708fb support user@host syntax;
wenzelm
parents: 64137
diff changeset
    29
        case _ => ("", s)
79cd4be708fb support user@host syntax;
wenzelm
parents: 64137
diff changeset
    30
      }
79cd4be708fb support user@host syntax;
wenzelm
parents: 64137
diff changeset
    31
79cd4be708fb support user@host syntax;
wenzelm
parents: 64137
diff changeset
    32
    def unapplySeq(s: String): Option[List[String]] =
64185
wenzelm
parents: 64166
diff changeset
    33
      parse(s) match {
wenzelm
parents: 64166
diff changeset
    34
        case (_, "") => None
wenzelm
parents: 64166
diff changeset
    35
        case (user, host) => Some(List(user, host))
wenzelm
parents: 64166
diff changeset
    36
      }
64141
79cd4be708fb support user@host syntax;
wenzelm
parents: 64137
diff changeset
    37
  }
79cd4be708fb support user@host syntax;
wenzelm
parents: 64137
diff changeset
    38
64142
954451356017 proper type for Library.using;
wenzelm
parents: 64141
diff changeset
    39
  val default_port = 22
67745
d83efbe52438 support for proxy connection, similar to ProxyCommand in ssh config;
wenzelm
parents: 67273
diff changeset
    40
  def make_port(port: Int): Int = if (port > 0) port else default_port
64142
954451356017 proper type for Library.using;
wenzelm
parents: 64141
diff changeset
    41
75500
57e292106d71 more operations;
wenzelm
parents: 75480
diff changeset
    42
  def port_suffix(port: Int): String =
57e292106d71 more operations;
wenzelm
parents: 75480
diff changeset
    43
    if (port == default_port) "" else ":" + port
71549
319599ba28cf more robust hg_url;
wenzelm
parents: 71383
diff changeset
    44
319599ba28cf more robust hg_url;
wenzelm
parents: 71383
diff changeset
    45
  def user_prefix(user: String): String =
319599ba28cf more robust hg_url;
wenzelm
parents: 71383
diff changeset
    46
    proper_string(user) match {
319599ba28cf more robust hg_url;
wenzelm
parents: 71383
diff changeset
    47
      case None => ""
319599ba28cf more robust hg_url;
wenzelm
parents: 71383
diff changeset
    48
      case Some(name) => name + "@"
319599ba28cf more robust hg_url;
wenzelm
parents: 71383
diff changeset
    49
    }
319599ba28cf more robust hg_url;
wenzelm
parents: 71383
diff changeset
    50
64257
9d51ac055cec tuned signature;
wenzelm
parents: 64256
diff changeset
    51
  def connect_timeout(options: Options): Int =
9d51ac055cec tuned signature;
wenzelm
parents: 64256
diff changeset
    52
    options.seconds("ssh_connect_timeout").ms.toInt
64141
79cd4be708fb support user@host syntax;
wenzelm
parents: 64137
diff changeset
    53
64325
47e03cb99274 prevent sporadic disconnection;
wenzelm
parents: 64306
diff changeset
    54
  def alive_interval(options: Options): Int =
47e03cb99274 prevent sporadic disconnection;
wenzelm
parents: 64306
diff changeset
    55
    options.seconds("ssh_alive_interval").ms.toInt
47e03cb99274 prevent sporadic disconnection;
wenzelm
parents: 64306
diff changeset
    56
67273
c573cfb2c407 more robust connection: prefer ServerAliveCountMax=3 (ssh default) instead of 1 (jsch default);
wenzelm
parents: 67067
diff 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: 67067
diff changeset
    58
    options.int("ssh_alive_count_max")
c573cfb2c407 more robust connection: prefer ServerAliveCountMax=3 (ssh default) instead of 1 (jsch default);
wenzelm
parents: 67067
diff changeset
    59
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    60
76115
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
    61
  /* open session */
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
    62
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
    63
  private def connect_session(
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
    64
    options: Options,
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
    65
    jsch: JSch,
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
    66
    host: String,
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
    67
    user: String = "",
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
    68
    port: Int = 0,
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
    69
    permissive: Boolean = false,
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
    70
    nominal_host: String = "",
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
    71
    nominal_user: String = "",
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
    72
    nominal_port: Option[Int] = None,
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
    73
    on_close: () => Unit = () => ()
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
    74
  ): Session = {
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
    75
    val connect_port = make_port(port)
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
    76
    val session = jsch.getSession(proper_string(user).orNull, host, connect_port)
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
    77
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
    78
    session.setUserInfo(No_User_Info)
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
    79
    session.setServerAliveInterval(alive_interval(options))
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
    80
    session.setServerAliveCountMax(alive_count_max(options))
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
    81
    session.setConfig("MaxAuthTries", "3")
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
    82
    if (permissive) session.setConfig("StrictHostKeyChecking", "no")
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
    83
    if (nominal_host != "") session.setHostKeyAlias(nominal_host)
64257
9d51ac055cec tuned signature;
wenzelm
parents: 64256
diff changeset
    84
76115
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
    85
    if (options.bool("ssh_compression")) {
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
    86
      session.setConfig("compression.s2c", "zlib@openssh.com,zlib,none")
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
    87
      session.setConfig("compression.c2s", "zlib@openssh.com,zlib,none")
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
    88
      session.setConfig("compression_level", "9")
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
    89
    }
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
    90
    session.connect(connect_timeout(options))
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
    91
    new Session(options, session, on_close,
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
    92
      proper_string(nominal_host) getOrElse host,
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
    93
      proper_string(nominal_user) getOrElse user,
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
    94
      nominal_port getOrElse connect_port)
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
    95
  }
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
    96
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
    97
  def open_session(
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
    98
    options: Options,
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
    99
    host: String,
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
   100
    user: String = "",
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
   101
    port: Int = 0,
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
   102
    actual_host: String = "",
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
   103
    proxy_host: String = "",
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
   104
    proxy_user: String = "",
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
   105
    proxy_port: Int = 0,
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
   106
    permissive: Boolean = false
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
   107
  ): Session = {
64130
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
   108
    val config_dir = Path.explode(options.string("ssh_config_dir"))
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   109
    if (!config_dir.is_dir) error("Bad ssh config directory: " + config_dir)
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   110
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   111
    val jsch = new JSch
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   112
64130
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
   113
    val config_file = Path.explode(options.string("ssh_config_file"))
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   114
    if (config_file.is_file)
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   115
      jsch.setConfigRepository(OpenSSHConfig.parseFile(File.platform_path(config_file)))
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   116
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   117
    val known_hosts = config_dir + Path.explode("known_hosts")
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   118
    if (!known_hosts.is_file) known_hosts.file.createNewFile
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   119
    jsch.setKnownHosts(File.platform_path(known_hosts))
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   120
64130
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
   121
    val identity_files =
71601
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71564
diff changeset
   122
      space_explode(':', options.string("ssh_identity_files")).map(Path.explode)
71780
21adf2ed442c more informative error;
wenzelm
parents: 71684
diff changeset
   123
    for (identity_file <- identity_files if identity_file.is_file) {
21adf2ed442c more informative error;
wenzelm
parents: 71684
diff changeset
   124
      try { jsch.addIdentity(File.platform_path(identity_file)) }
21adf2ed442c more informative error;
wenzelm
parents: 71684
diff changeset
   125
      catch {
21adf2ed442c more informative error;
wenzelm
parents: 71684
diff changeset
   126
        case exn: JSchException =>
21adf2ed442c more informative error;
wenzelm
parents: 71684
diff changeset
   127
          error("Error in ssh identity file " + identity_file + ": " + exn.getMessage)
21adf2ed442c more informative error;
wenzelm
parents: 71684
diff changeset
   128
      }
21adf2ed442c more informative error;
wenzelm
parents: 71684
diff changeset
   129
    }
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   130
76115
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
   131
    val connect_host = proper_string(actual_host) getOrElse host
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
   132
    val connect_port = make_port(port)
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
   133
    if (proxy_host == "") {
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
   134
      connect_session(options, jsch, host = connect_host, user = user, port = connect_port)
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
   135
    }
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
   136
    else {
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
   137
      val proxy =
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
   138
        connect_session(options, jsch, host = proxy_host, port = proxy_port, user = proxy_user)
67067
02729ced9b1e tuned signature;
wenzelm
parents: 67066
diff changeset
   139
76115
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
   140
      val fw =
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
   141
        try { proxy.port_forwarding(remote_host = connect_host, remote_port = connect_port) }
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
   142
        catch { case exn: Throwable => proxy.close(); throw exn }
64257
9d51ac055cec tuned signature;
wenzelm
parents: 64256
diff changeset
   143
76115
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
   144
      try {
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
   145
        connect_session(options, jsch,
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
   146
          host = fw.local_host,
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
   147
          port = fw.local_port,
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
   148
          permissive = permissive,
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
   149
          nominal_host = host,
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
   150
          nominal_port = Some(connect_port),
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
   151
          nominal_user = user, user = user,
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
   152
          on_close = { () => fw.close(); proxy.close() })
64257
9d51ac055cec tuned signature;
wenzelm
parents: 64256
diff changeset
   153
      }
76115
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
   154
      catch { case exn: Throwable => fw.close(); proxy.close(); throw exn }
64257
9d51ac055cec tuned signature;
wenzelm
parents: 64256
diff changeset
   155
    }
9d51ac055cec tuned signature;
wenzelm
parents: 64256
diff changeset
   156
  }
64130
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
   157
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   158
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   159
  /* logging */
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   160
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74306
diff changeset
   161
  def logging(verbose: Boolean = true, debug: Boolean = false): Unit = {
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   162
    JSch.setLogger(if (verbose) new Logger(debug) else null)
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   163
  }
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   164
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74306
diff changeset
   165
  private class Logger(debug: Boolean) extends JSch_Logger {
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   166
    def isEnabled(level: Int): Boolean = level != JSch_Logger.DEBUG || debug
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   167
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74306
diff changeset
   168
    def log(level: Int, msg: String): Unit = {
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   169
      level match {
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   170
        case JSch_Logger.ERROR | JSch_Logger.FATAL => Output.error_message(msg)
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   171
        case JSch_Logger.WARN => Output.warning(msg)
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   172
        case _ => Output.writeln(msg)
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   173
      }
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   174
    }
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   175
  }
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   176
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   177
64128
wenzelm
parents: 64127
diff changeset
   178
  /* user info */
wenzelm
parents: 64127
diff changeset
   179
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74306
diff changeset
   180
  object No_User_Info extends UserInfo {
64128
wenzelm
parents: 64127
diff changeset
   181
    def getPassphrase: String = null
wenzelm
parents: 64127
diff changeset
   182
    def getPassword: String = null
wenzelm
parents: 64127
diff changeset
   183
    def promptPassword(msg: String): Boolean = false
wenzelm
parents: 64127
diff changeset
   184
    def promptPassphrase(msg: String): Boolean = false
wenzelm
parents: 64127
diff changeset
   185
    def promptYesNo(msg: String): Boolean = false
wenzelm
parents: 64127
diff changeset
   186
    def showMessage(msg: String): Unit = Output.writeln(msg)
wenzelm
parents: 64127
diff changeset
   187
  }
wenzelm
parents: 64127
diff changeset
   188
wenzelm
parents: 64127
diff changeset
   189
64191
wenzelm
parents: 64190
diff changeset
   190
  /* Sftp channel */
wenzelm
parents: 64190
diff changeset
   191
wenzelm
parents: 64190
diff changeset
   192
  type Attrs = SftpATTRS
wenzelm
parents: 64190
diff changeset
   193
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74306
diff changeset
   194
  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: 67771
diff changeset
   195
    def is_file: Boolean = !is_dir
64191
wenzelm
parents: 64190
diff changeset
   196
  }
wenzelm
parents: 64190
diff changeset
   197
wenzelm
parents: 64190
diff changeset
   198
64132
c2594513687b more Sftp operations;
wenzelm
parents: 64131
diff changeset
   199
  /* exec channel */
c2594513687b more Sftp operations;
wenzelm
parents: 64131
diff changeset
   200
64134
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   201
  private val exec_wait_delay = Time.seconds(0.3)
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   202
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74306
diff changeset
   203
  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: 64254
diff changeset
   204
    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: 64254
diff changeset
   205
75548
wenzelm
parents: 75547
diff changeset
   206
    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: 64254
diff changeset
   207
64134
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   208
    val exit_status: Future[Int] =
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   209
      Future.thread("ssh_wait") {
73702
7202e12cb324 tuned signature --- following hints by IntelliJ IDEA;
wenzelm
parents: 73634
diff changeset
   210
        while (!channel.isClosed) exec_wait_delay.sleep()
64134
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   211
        channel.getExitStatus
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   212
      }
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   213
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   214
    val stdin: OutputStream = channel.getOutputStream
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   215
    val stdout: InputStream = channel.getInputStream
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   216
    val stderr: InputStream = channel.getErrStream
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   217
64166
44925cf6ded1 tuned signature;
wenzelm
parents: 64142
diff changeset
   218
    // connect after preparing streams
44925cf6ded1 tuned signature;
wenzelm
parents: 64142
diff changeset
   219
    channel.connect(connect_timeout(session.options))
64134
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   220
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   221
    def result(
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   222
      progress_stdout: String => Unit = (_: String) => (),
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   223
      progress_stderr: String => Unit = (_: String) => (),
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74306
diff changeset
   224
      strict: Boolean = true
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74306
diff changeset
   225
    ): Process_Result = {
73367
77ef8bef0593 clarified signature --- fewer warnings;
wenzelm
parents: 73340
diff changeset
   226
      stdin.close()
64134
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   227
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74306
diff changeset
   228
      def read_lines(stream: InputStream, progress: String => Unit): List[String] = {
64134
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   229
        val result = new mutable.ListBuffer[String]
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   230
        val line_buffer = new ByteArrayOutputStream(100)
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74306
diff changeset
   231
        def line_flush(): Unit = {
64326
ff3c383b9163 extra trim_line for the sake of Windows;
wenzelm
parents: 64325
diff changeset
   232
          val line = Library.trim_line(line_buffer.toString(UTF8.charset_name))
64134
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   233
          progress(line)
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   234
          result += line
75548
wenzelm
parents: 75547
diff changeset
   235
          line_buffer.reset()
64134
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   236
        }
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   237
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   238
        var c = 0
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   239
        var finished = false
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   240
        while (!finished) {
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   241
          while ({ c = stream.read; c != -1 && c != 10 }) line_buffer.write(c)
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   242
          if (c == 10) line_flush()
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   243
          else if (channel.isClosed) {
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   244
            if (line_buffer.size > 0) line_flush()
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   245
            finished = true
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   246
          }
73702
7202e12cb324 tuned signature --- following hints by IntelliJ IDEA;
wenzelm
parents: 73634
diff changeset
   247
          else exec_wait_delay.sleep()
64134
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   248
        }
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   249
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   250
        result.toList
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   251
      }
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   252
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   253
      val out_lines = Future.thread("ssh_stdout") { read_lines(stdout, progress_stdout) }
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   254
      val err_lines = Future.thread("ssh_stderr") { read_lines(stderr, progress_stderr) }
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   255
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74306
diff changeset
   256
      def terminate(): Unit = {
73367
77ef8bef0593 clarified signature --- fewer warnings;
wenzelm
parents: 73340
diff changeset
   257
        close()
64134
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   258
        out_lines.join
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   259
        err_lines.join
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   260
        exit_status.join
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   261
      }
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   262
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   263
      val rc =
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   264
        try { exit_status.join }
74306
a117c076aa22 clarified signature;
wenzelm
parents: 74067
diff changeset
   265
        catch { case Exn.Interrupt() => terminate(); Process_Result.RC.interrupt }
64134
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   266
73367
77ef8bef0593 clarified signature --- fewer warnings;
wenzelm
parents: 73340
diff changeset
   267
      close()
74306
a117c076aa22 clarified signature;
wenzelm
parents: 74067
diff changeset
   268
      if (strict && rc == Process_Result.RC.interrupt) throw Exn.Interrupt()
64134
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   269
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   270
      Process_Result(rc, out_lines.join, err_lines.join)
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   271
    }
64131
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
   272
  }
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
   273
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
   274
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   275
  /* session */
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   276
67745
d83efbe52438 support for proxy connection, similar to ProxyCommand in ssh config;
wenzelm
parents: 67273
diff changeset
   277
  class Session private[SSH](
d83efbe52438 support for proxy connection, similar to ProxyCommand in ssh config;
wenzelm
parents: 67273
diff changeset
   278
    val options: Options,
76116
c4dc343fdbcb clarified signature: avoid exposure of JSch types;
wenzelm
parents: 76115
diff changeset
   279
    session: JSch_Session,
71549
319599ba28cf more robust hg_url;
wenzelm
parents: 71383
diff changeset
   280
    on_close: () => Unit,
319599ba28cf more robust hg_url;
wenzelm
parents: 71383
diff changeset
   281
    val nominal_host: String,
75544
179a3b028b0a proper nominal_port, notably for port forwarding;
wenzelm
parents: 75517
diff changeset
   282
    val nominal_user: String,
179a3b028b0a proper nominal_port, notably for port forwarding;
wenzelm
parents: 75517
diff changeset
   283
    val nominal_port: Int
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74306
diff changeset
   284
  ) extends System {
76116
c4dc343fdbcb clarified signature: avoid exposure of JSch types;
wenzelm
parents: 76115
diff changeset
   285
    ssh =>
c4dc343fdbcb clarified signature: avoid exposure of JSch types;
wenzelm
parents: 76115
diff changeset
   286
64347
602483aa7818 support for URL notation;
wenzelm
parents: 64326
diff changeset
   287
    def host: String = if (session.getHost == null) "" else session.getHost
71549
319599ba28cf more robust hg_url;
wenzelm
parents: 71383
diff changeset
   288
319599ba28cf more robust hg_url;
wenzelm
parents: 71383
diff changeset
   289
    override def hg_url: String =
319599ba28cf more robust hg_url;
wenzelm
parents: 71383
diff changeset
   290
      "ssh://" + user_prefix(nominal_user) + nominal_host + "/"
66570
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   291
75500
57e292106d71 more operations;
wenzelm
parents: 75480
diff changeset
   292
    override def rsync_prefix: String =
57e292106d71 more operations;
wenzelm
parents: 75480
diff changeset
   293
      user_prefix(nominal_user) + nominal_host + ":"
57e292106d71 more operations;
wenzelm
parents: 75480
diff changeset
   294
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   295
    override def toString: String =
75544
179a3b028b0a proper nominal_port, notably for port forwarding;
wenzelm
parents: 75517
diff changeset
   296
      user_prefix(session.getUserName) + host + port_suffix(session.getPort) +
71549
319599ba28cf more robust hg_url;
wenzelm
parents: 71383
diff changeset
   297
      (if (session.isConnected) "" else " (disconnected)")
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   298
64256
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   299
65009
eda9366bbfac remote database access via ssh port forwarding;
wenzelm
parents: 64347
diff changeset
   300
    /* port forwarding */
eda9366bbfac remote database access via ssh port forwarding;
wenzelm
parents: 64347
diff changeset
   301
65636
df804cdba5f9 ssh_close for proper termination after use of database;
wenzelm
parents: 65594
diff changeset
   302
    def port_forwarding(
76116
c4dc343fdbcb clarified signature: avoid exposure of JSch types;
wenzelm
parents: 76115
diff changeset
   303
      remote_port: Int,
c4dc343fdbcb clarified signature: avoid exposure of JSch types;
wenzelm
parents: 76115
diff changeset
   304
      remote_host: String = "localhost",
c4dc343fdbcb clarified signature: avoid exposure of JSch types;
wenzelm
parents: 76115
diff changeset
   305
      local_port: Int = 0,
c4dc343fdbcb clarified signature: avoid exposure of JSch types;
wenzelm
parents: 76115
diff changeset
   306
      local_host: String = "localhost",
c4dc343fdbcb clarified signature: avoid exposure of JSch types;
wenzelm
parents: 76115
diff changeset
   307
      ssh_close: Boolean = false
c4dc343fdbcb clarified signature: avoid exposure of JSch types;
wenzelm
parents: 76115
diff changeset
   308
    ): Port_Forwarding = {
c4dc343fdbcb clarified signature: avoid exposure of JSch types;
wenzelm
parents: 76115
diff changeset
   309
      val local_port1 = session.setPortForwardingL(local_host, local_port, remote_host, remote_port)
c4dc343fdbcb clarified signature: avoid exposure of JSch types;
wenzelm
parents: 76115
diff changeset
   310
      new Port_Forwarding(local_host, local_port1, remote_host, remote_port) {
c4dc343fdbcb clarified signature: avoid exposure of JSch types;
wenzelm
parents: 76115
diff changeset
   311
        override def close(): Unit = {
c4dc343fdbcb clarified signature: avoid exposure of JSch types;
wenzelm
parents: 76115
diff changeset
   312
          session.delPortForwardingL(this.local_host, this.local_port)
c4dc343fdbcb clarified signature: avoid exposure of JSch types;
wenzelm
parents: 76115
diff changeset
   313
          if (ssh_close) ssh.close()
c4dc343fdbcb clarified signature: avoid exposure of JSch types;
wenzelm
parents: 76115
diff changeset
   314
        }
c4dc343fdbcb clarified signature: avoid exposure of JSch types;
wenzelm
parents: 76115
diff changeset
   315
      }
c4dc343fdbcb clarified signature: avoid exposure of JSch types;
wenzelm
parents: 76115
diff changeset
   316
    }
65009
eda9366bbfac remote database access via ssh port forwarding;
wenzelm
parents: 64347
diff changeset
   317
eda9366bbfac remote database access via ssh port forwarding;
wenzelm
parents: 64347
diff changeset
   318
64256
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   319
    /* sftp channel */
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   320
76116
c4dc343fdbcb clarified signature: avoid exposure of JSch types;
wenzelm
parents: 76115
diff changeset
   321
    private val sftp: ChannelSftp = session.openChannel("sftp").asInstanceOf[ChannelSftp]
64256
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   322
    sftp.connect(connect_timeout(options))
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   323
75548
wenzelm
parents: 75547
diff changeset
   324
    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: 64254
diff changeset
   325
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74306
diff changeset
   326
    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: 64254
diff changeset
   327
      val home = sftp.getHome
73897
0ddb5de0506e clarified signature: prefer Java interfaces;
wenzelm
parents: 73702
diff changeset
   328
      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: 64254
diff changeset
   329
    }
66570
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   330
    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: 64254
diff changeset
   331
    def remote_path(path: Path): String = expand_path(path).implode
67066
1645cef7a49c proper ssh.bash_path;
wenzelm
parents: 66923
diff changeset
   332
    override def bash_path(path: Path): String = Bash.string(remote_path(path))
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   333
64256
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   334
    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: 64254
diff changeset
   335
    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: 64254
diff changeset
   336
    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: 64254
diff changeset
   337
    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: 64254
diff changeset
   338
    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: 64254
diff changeset
   339
69302
5faf57207a9b proper use of stat() vs. lstat() (for symlinks);
wenzelm
parents: 69301
diff changeset
   340
    private def test_entry(path: Path, as_dir: Boolean): Boolean =
5faf57207a9b proper use of stat() vs. lstat() (for symlinks);
wenzelm
parents: 69301
diff changeset
   341
      try {
5faf57207a9b proper use of stat() vs. lstat() (for symlinks);
wenzelm
parents: 69301
diff changeset
   342
        val is_dir = sftp.stat(remote_path(path)).isDir
5faf57207a9b proper use of stat() vs. lstat() (for symlinks);
wenzelm
parents: 69301
diff changeset
   343
        if (as_dir) is_dir else !is_dir
5faf57207a9b proper use of stat() vs. lstat() (for symlinks);
wenzelm
parents: 69301
diff changeset
   344
      }
5faf57207a9b proper use of stat() vs. lstat() (for symlinks);
wenzelm
parents: 69301
diff changeset
   345
      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: 67771
diff changeset
   346
69302
5faf57207a9b proper use of stat() vs. lstat() (for symlinks);
wenzelm
parents: 69301
diff changeset
   347
    override def is_dir(path: Path): Boolean = test_entry(path, true)
5faf57207a9b proper use of stat() vs. lstat() (for symlinks);
wenzelm
parents: 69301
diff changeset
   348
    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: 67771
diff changeset
   349
69301
f6c17b9e1104 more uniform find_files, notably for symlinks;
wenzelm
parents: 69300
diff changeset
   350
    def is_link(path: Path): Boolean =
f6c17b9e1104 more uniform find_files, notably for symlinks;
wenzelm
parents: 69300
diff changeset
   351
      try { sftp.lstat(remote_path(path)).isLink }
f6c17b9e1104 more uniform find_files, notably for symlinks;
wenzelm
parents: 69300
diff changeset
   352
      catch { case _: SftpException => false }
f6c17b9e1104 more uniform find_files, notably for symlinks;
wenzelm
parents: 69300
diff changeset
   353
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74306
diff changeset
   354
    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: 64254
diff changeset
   355
      if (!is_dir(path)) {
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   356
        execute(
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   357
          "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: 64254
diff changeset
   358
        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: 64254
diff changeset
   359
      }
72376
04bce3478688 clarified signature;
wenzelm
parents: 72375
diff changeset
   360
      path
04bce3478688 clarified signature;
wenzelm
parents: 72375
diff changeset
   361
    }
64256
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   362
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74306
diff changeset
   363
    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: 67771
diff changeset
   364
      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: 67771
diff changeset
   365
8b6ab9989bcd is_file/is_dir/read_dir: more uniform treatment of errors and boundary cases, notably for symlinks in ssh;
wenzelm
parents: 67771
diff changeset
   366
      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: 67771
diff changeset
   367
      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: 64254
diff changeset
   368
      (for {
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   369
        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: 64254
diff changeset
   370
        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: 64254
diff changeset
   371
        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: 64254
diff changeset
   372
        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: 64254
diff changeset
   373
        if name != "." && name != ".."
69302
5faf57207a9b proper use of stat() vs. lstat() (for symlinks);
wenzelm
parents: 69301
diff changeset
   374
      }
5faf57207a9b proper use of stat() vs. lstat() (for symlinks);
wenzelm
parents: 69301
diff changeset
   375
      yield {
5faf57207a9b proper use of stat() vs. lstat() (for symlinks);
wenzelm
parents: 69301
diff changeset
   376
        Dir_Entry(name,
5faf57207a9b proper use of stat() vs. lstat() (for symlinks);
wenzelm
parents: 69301
diff changeset
   377
          if (attrs.isLink) {
5faf57207a9b proper use of stat() vs. lstat() (for symlinks);
wenzelm
parents: 69301
diff changeset
   378
            try { sftp.stat(dir_name + "/" + name).isDir }
5faf57207a9b proper use of stat() vs. lstat() (for symlinks);
wenzelm
parents: 69301
diff changeset
   379
            catch { case _: SftpException => false }
5faf57207a9b proper use of stat() vs. lstat() (for symlinks);
wenzelm
parents: 69301
diff changeset
   380
          }
5faf57207a9b proper use of stat() vs. lstat() (for symlinks);
wenzelm
parents: 69301
diff changeset
   381
          else attrs.isDir)
69427
ff2f39a221d4 clarified operations: uniform sorting of results;
wenzelm
parents: 69393
diff changeset
   382
      }).toList.sortBy(_.name)
64191
wenzelm
parents: 64190
diff changeset
   383
    }
64135
865dda40e1cc provide execute operation, similar to Isabelle_System.bash;
wenzelm
parents: 64134
diff changeset
   384
69301
f6c17b9e1104 more uniform find_files, notably for symlinks;
wenzelm
parents: 69300
diff changeset
   385
    def find_files(
f6c17b9e1104 more uniform find_files, notably for symlinks;
wenzelm
parents: 69300
diff changeset
   386
      start: Path,
f6c17b9e1104 more uniform find_files, notably for symlinks;
wenzelm
parents: 69300
diff changeset
   387
      pred: Path => Boolean = _ => true,
f6c17b9e1104 more uniform find_files, notably for symlinks;
wenzelm
parents: 69300
diff changeset
   388
      include_dirs: Boolean = false,
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74306
diff changeset
   389
      follow_links: Boolean = false
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74306
diff changeset
   390
    ): List[Path] = {
69301
f6c17b9e1104 more uniform find_files, notably for symlinks;
wenzelm
parents: 69300
diff changeset
   391
      val result = new mutable.ListBuffer[Path]
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 72376
diff changeset
   392
      def check(path: Path): Unit = { if (pred(path)) result += path }
69301
f6c17b9e1104 more uniform find_files, notably for symlinks;
wenzelm
parents: 69300
diff changeset
   393
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74306
diff changeset
   394
      def find(dir: Path): Unit = {
69303
51d8b4dbc61b more uniform wrt. File.find_files;
wenzelm
parents: 69302
diff changeset
   395
        if (include_dirs) check(dir)
69301
f6c17b9e1104 more uniform find_files, notably for symlinks;
wenzelm
parents: 69300
diff changeset
   396
        if (follow_links || !is_link(dir)) {
f6c17b9e1104 more uniform find_files, notably for symlinks;
wenzelm
parents: 69300
diff changeset
   397
          for (entry <- read_dir(dir)) {
69302
5faf57207a9b proper use of stat() vs. lstat() (for symlinks);
wenzelm
parents: 69301
diff changeset
   398
            val path = dir + Path.basic(entry.name)
5faf57207a9b proper use of stat() vs. lstat() (for symlinks);
wenzelm
parents: 69301
diff changeset
   399
            if (entry.is_file) check(path) else find(path)
69301
f6c17b9e1104 more uniform find_files, notably for symlinks;
wenzelm
parents: 69300
diff changeset
   400
          }
f6c17b9e1104 more uniform find_files, notably for symlinks;
wenzelm
parents: 69300
diff changeset
   401
        }
f6c17b9e1104 more uniform find_files, notably for symlinks;
wenzelm
parents: 69300
diff changeset
   402
      }
f6c17b9e1104 more uniform find_files, notably for symlinks;
wenzelm
parents: 69300
diff changeset
   403
      if (is_file(start)) check(start) else find(start)
f6c17b9e1104 more uniform find_files, notably for symlinks;
wenzelm
parents: 69300
diff changeset
   404
f6c17b9e1104 more uniform find_files, notably for symlinks;
wenzelm
parents: 69300
diff changeset
   405
      result.toList
64256
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   406
    }
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   407
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   408
    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: 64254
diff changeset
   409
    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: 64254
diff changeset
   410
73634
c88faa1e09e1 support local build_heaps;
wenzelm
parents: 73367
diff changeset
   411
    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: 64254
diff changeset
   412
      sftp.get(remote_path(path), File.platform_path(local_path))
75513
36316c6a3fc2 clarified signature: more operations;
wenzelm
parents: 75500
diff changeset
   413
    override def read_bytes(path: Path): Bytes = using(open_input(path))(Bytes.read_stream(_))
36316c6a3fc2 clarified signature: more operations;
wenzelm
parents: 75500
diff changeset
   414
    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: 64254
diff changeset
   415
73634
c88faa1e09e1 support local build_heaps;
wenzelm
parents: 73367
diff changeset
   416
    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: 64254
diff changeset
   417
      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: 64254
diff changeset
   418
    def write_bytes(path: Path, bytes: Bytes): Unit =
71601
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71564
diff changeset
   419
      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: 64254
diff changeset
   420
    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: 64254
diff changeset
   421
      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: 64254
diff changeset
   422
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   423
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   424
    /* exec channel */
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   425
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74306
diff changeset
   426
    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: 64254
diff changeset
   427
      val channel = session.openChannel("exec").asInstanceOf[ChannelExec]
64190
c62b99e3ec07 provide USER_HOME, such that symbolic Path.explode("~") can be used remotely;
wenzelm
parents: 64185
diff changeset
   428
      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: 64254
diff changeset
   429
      new Exec(this, channel)
64129
fce8b7c746b4 support for remote command execution;
wenzelm
parents: 64128
diff changeset
   430
    }
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   431
66570
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   432
    override def execute(command: String,
64191
wenzelm
parents: 64190
diff changeset
   433
        progress_stdout: String => Unit = (_: String) => (),
wenzelm
parents: 64190
diff changeset
   434
        progress_stderr: String => Unit = (_: String) => (),
73634
c88faa1e09e1 support local build_heaps;
wenzelm
parents: 73367
diff changeset
   435
        settings: Boolean = true,
64191
wenzelm
parents: 64190
diff changeset
   436
        strict: Boolean = true): Process_Result =
wenzelm
parents: 64190
diff changeset
   437
      exec(command).result(progress_stdout, progress_stderr, strict)
64137
e9b3d9c1bc5a support for remote tmp dirs;
wenzelm
parents: 64136
diff changeset
   438
72340
676066aa4798 clarified signature;
wenzelm
parents: 72338
diff changeset
   439
    override def isabelle_platform: Isabelle_Platform = Isabelle_Platform(ssh = Some(this))
72338
54871a086193 formal platform information, notably for ssh;
wenzelm
parents: 71780
diff changeset
   440
64137
e9b3d9c1bc5a support for remote tmp dirs;
wenzelm
parents: 64136
diff changeset
   441
e9b3d9c1bc5a support for remote tmp dirs;
wenzelm
parents: 64136
diff changeset
   442
    /* tmp dirs */
e9b3d9c1bc5a support for remote tmp dirs;
wenzelm
parents: 64136
diff changeset
   443
64306
7b6dc1b36f20 tuned signature, in accordance to Isabelle_System;
wenzelm
parents: 64304
diff changeset
   444
    def rm_tree(dir: Path): Unit = rm_tree(remote_path(dir))
7b6dc1b36f20 tuned signature, in accordance to Isabelle_System;
wenzelm
parents: 64304
diff changeset
   445
64137
e9b3d9c1bc5a support for remote tmp dirs;
wenzelm
parents: 64136
diff changeset
   446
    def rm_tree(remote_dir: String): Unit =
64304
96bc94c87a81 clarified modules;
wenzelm
parents: 64258
diff changeset
   447
      execute("rm -r -f " + Bash.string(remote_dir)).check
64137
e9b3d9c1bc5a support for remote tmp dirs;
wenzelm
parents: 64136
diff changeset
   448
e9b3d9c1bc5a support for remote tmp dirs;
wenzelm
parents: 64136
diff changeset
   449
    def tmp_dir(): String =
e9b3d9c1bc5a support for remote tmp dirs;
wenzelm
parents: 64136
diff changeset
   450
      execute("mktemp -d -t tmp.XXXXXXXXXX").check.out
e9b3d9c1bc5a support for remote tmp dirs;
wenzelm
parents: 64136
diff changeset
   451
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74306
diff changeset
   452
    override def with_tmp_dir[A](body: Path => A): A = {
64137
e9b3d9c1bc5a support for remote tmp dirs;
wenzelm
parents: 64136
diff changeset
   453
      val remote_dir = tmp_dir()
64233
ef6f7e8a018c clarified signature: more static types;
wenzelm
parents: 64228
diff changeset
   454
      try { body(Path.explode(remote_dir)) } finally { rm_tree(remote_dir) }
64137
e9b3d9c1bc5a support for remote tmp dirs;
wenzelm
parents: 64136
diff changeset
   455
    }
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   456
  }
66570
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   457
76116
c4dc343fdbcb clarified signature: avoid exposure of JSch types;
wenzelm
parents: 76115
diff changeset
   458
  abstract class Port_Forwarding private[SSH](
c4dc343fdbcb clarified signature: avoid exposure of JSch types;
wenzelm
parents: 76115
diff changeset
   459
    val local_host: String,
c4dc343fdbcb clarified signature: avoid exposure of JSch types;
wenzelm
parents: 76115
diff changeset
   460
    val local_port: Int,
c4dc343fdbcb clarified signature: avoid exposure of JSch types;
wenzelm
parents: 76115
diff changeset
   461
    val remote_host: String,
c4dc343fdbcb clarified signature: avoid exposure of JSch types;
wenzelm
parents: 76115
diff changeset
   462
    val remote_port: Int
c4dc343fdbcb clarified signature: avoid exposure of JSch types;
wenzelm
parents: 76115
diff changeset
   463
  ) extends AutoCloseable {
c4dc343fdbcb clarified signature: avoid exposure of JSch types;
wenzelm
parents: 76115
diff changeset
   464
    override def toString: String =
c4dc343fdbcb clarified signature: avoid exposure of JSch types;
wenzelm
parents: 76115
diff changeset
   465
      local_host + ":" + local_port + ":" + remote_host + ":" + remote_port
c4dc343fdbcb clarified signature: avoid exposure of JSch types;
wenzelm
parents: 76115
diff changeset
   466
  }
c4dc343fdbcb clarified signature: avoid exposure of JSch types;
wenzelm
parents: 76115
diff changeset
   467
66570
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   468
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   469
  /* system operations */
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   470
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74306
diff changeset
   471
  trait System extends AutoCloseable {
73634
c88faa1e09e1 support local build_heaps;
wenzelm
parents: 73367
diff changeset
   472
    def close(): Unit = ()
c88faa1e09e1 support local build_heaps;
wenzelm
parents: 73367
diff changeset
   473
66570
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   474
    def hg_url: String = ""
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   475
75500
57e292106d71 more operations;
wenzelm
parents: 75480
diff changeset
   476
    def rsync_prefix: String = ""
75517
292d7a9dc8a3 proper operation on String, not Path;
wenzelm
parents: 75513
diff changeset
   477
    def rsync_path(path: Path): String = rsync_prefix + expand_path(path).implode
75500
57e292106d71 more operations;
wenzelm
parents: 75480
diff changeset
   478
66570
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   479
    def expand_path(path: Path): Path = path.expand
67066
1645cef7a49c proper ssh.bash_path;
wenzelm
parents: 66923
diff changeset
   480
    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: 67771
diff changeset
   481
    def is_dir(path: Path): Boolean = path.is_dir
66570
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   482
    def is_file(path: Path): Boolean = path.is_file
72376
04bce3478688 clarified signature;
wenzelm
parents: 72375
diff changeset
   483
    def make_directory(path: Path): Path = Isabelle_System.make_directory(path)
73634
c88faa1e09e1 support local build_heaps;
wenzelm
parents: 73367
diff changeset
   484
    def with_tmp_dir[A](body: Path => A): A = Isabelle_System.with_tmp_dir("tmp")(body)
c88faa1e09e1 support local build_heaps;
wenzelm
parents: 73367
diff changeset
   485
    def read_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path1, path2)
c88faa1e09e1 support local build_heaps;
wenzelm
parents: 73367
diff changeset
   486
    def write_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path2, path1)
75513
36316c6a3fc2 clarified signature: more operations;
wenzelm
parents: 75500
diff changeset
   487
    def read_bytes(path: Path): Bytes = Bytes.read(path)
36316c6a3fc2 clarified signature: more operations;
wenzelm
parents: 75500
diff changeset
   488
    def read(path: Path): String = File.read(path)
66570
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   489
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   490
    def execute(command: String,
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   491
        progress_stdout: String => Unit = (_: String) => (),
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   492
        progress_stderr: String => Unit = (_: String) => (),
73634
c88faa1e09e1 support local build_heaps;
wenzelm
parents: 73367
diff changeset
   493
        settings: Boolean = true,
66570
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   494
        strict: Boolean = true): Process_Result =
73634
c88faa1e09e1 support local build_heaps;
wenzelm
parents: 73367
diff changeset
   495
      Isabelle_System.bash(command,
c88faa1e09e1 support local build_heaps;
wenzelm
parents: 73367
diff changeset
   496
        progress_stdout = progress_stdout,
c88faa1e09e1 support local build_heaps;
wenzelm
parents: 73367
diff changeset
   497
        progress_stderr = progress_stderr,
c88faa1e09e1 support local build_heaps;
wenzelm
parents: 73367
diff changeset
   498
        env = if (settings) Isabelle_System.settings() else null,
c88faa1e09e1 support local build_heaps;
wenzelm
parents: 73367
diff changeset
   499
        strict = strict)
72338
54871a086193 formal platform information, notably for ssh;
wenzelm
parents: 71780
diff changeset
   500
72340
676066aa4798 clarified signature;
wenzelm
parents: 72338
diff changeset
   501
    def isabelle_platform: Isabelle_Platform = Isabelle_Platform()
66570
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   502
  }
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   503
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   504
  object Local extends System
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   505
}