src/Pure/General/ssh.scala
author wenzelm
Mon, 10 Oct 2016 14:45:32 +0200
changeset 64131 f01fca58e0a5
parent 64130 e17c211a0bb6
child 64132 c2594513687b
permissions -rw-r--r--
more specific channels; more Sftp operations;
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
64131
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
    10
import java.io.{InputStream, OutputStream}
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
    11
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
    12
import scala.collection.JavaConversions
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
    13
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    14
import com.jcraft.jsch.{JSch, Logger => JSch_Logger, Session => JSch_Session,
64130
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
    15
  OpenSSHConfig, UserInfo, Channel => JSch_Channel, ChannelExec, ChannelSftp}
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    16
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    17
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    18
object SSH
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    19
{
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    20
  /* init */
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    21
64130
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
    22
  def init(options: Options): SSH =
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    23
  {
64130
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
    24
    val config_dir = Path.explode(options.string("ssh_config_dir"))
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    25
    if (!config_dir.is_dir) error("Bad ssh config directory: " + config_dir)
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    26
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    27
    val jsch = new JSch
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    28
64130
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
    29
    val config_file = Path.explode(options.string("ssh_config_file"))
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    30
    if (config_file.is_file)
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    31
      jsch.setConfigRepository(OpenSSHConfig.parseFile(File.platform_path(config_file)))
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    32
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    33
    val known_hosts = config_dir + Path.explode("known_hosts")
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    34
    if (!known_hosts.is_file) known_hosts.file.createNewFile
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    35
    jsch.setKnownHosts(File.platform_path(known_hosts))
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    36
64130
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
    37
    val identity_files =
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
    38
      Library.space_explode(':', options.string("ssh_identity_files")).map(Path.explode(_))
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    39
    for (identity_file <- identity_files if identity_file.is_file)
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    40
      jsch.addIdentity(File.platform_path(identity_file))
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    41
64130
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
    42
    new SSH(options, jsch)
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    43
  }
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    44
64130
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
    45
  def connect_timeout(options: Options): Int =
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
    46
    options.seconds("ssh_connect_timeout").ms.toInt
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
    47
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    48
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    49
  /* logging */
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    50
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    51
  def logging(verbose: Boolean = true, debug: Boolean = false)
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    52
  {
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    53
    JSch.setLogger(if (verbose) new Logger(debug) else null)
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    54
  }
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    55
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    56
  private class Logger(debug: Boolean) extends JSch_Logger
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    57
  {
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    58
    def isEnabled(level: Int): Boolean = level != JSch_Logger.DEBUG || debug
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    59
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    60
    def log(level: Int, msg: String)
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    61
    {
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    62
      level match {
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    63
        case JSch_Logger.ERROR | JSch_Logger.FATAL => Output.error_message(msg)
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    64
        case JSch_Logger.WARN => Output.warning(msg)
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    65
        case _ => Output.writeln(msg)
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    66
      }
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    67
    }
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    68
  }
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    69
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    70
64128
wenzelm
parents: 64127
diff changeset
    71
  /* user info */
wenzelm
parents: 64127
diff changeset
    72
wenzelm
parents: 64127
diff changeset
    73
  object No_User_Info extends UserInfo
wenzelm
parents: 64127
diff changeset
    74
  {
wenzelm
parents: 64127
diff changeset
    75
    def getPassphrase: String = null
wenzelm
parents: 64127
diff changeset
    76
    def getPassword: String = null
wenzelm
parents: 64127
diff changeset
    77
    def promptPassword(msg: String): Boolean = false
wenzelm
parents: 64127
diff changeset
    78
    def promptPassphrase(msg: String): Boolean = false
wenzelm
parents: 64127
diff changeset
    79
    def promptYesNo(msg: String): Boolean = false
wenzelm
parents: 64127
diff changeset
    80
    def showMessage(msg: String): Unit = Output.writeln(msg)
wenzelm
parents: 64127
diff changeset
    81
  }
wenzelm
parents: 64127
diff changeset
    82
wenzelm
parents: 64127
diff changeset
    83
64130
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
    84
  /* channel: exec, sftp etc. */
64129
fce8b7c746b4 support for remote command execution;
wenzelm
parents: 64128
diff changeset
    85
64130
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
    86
  class Channel[C <: JSch_Channel] private[SSH](val session: Session,
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
    87
    val kind: String, val channel_options: Options, val channel: C)
64129
fce8b7c746b4 support for remote command execution;
wenzelm
parents: 64128
diff changeset
    88
  {
64130
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
    89
    override def toString: String = kind + " " + session.toString
64129
fce8b7c746b4 support for remote command execution;
wenzelm
parents: 64128
diff changeset
    90
fce8b7c746b4 support for remote command execution;
wenzelm
parents: 64128
diff changeset
    91
    def close { channel.disconnect }
fce8b7c746b4 support for remote command execution;
wenzelm
parents: 64128
diff changeset
    92
  }
fce8b7c746b4 support for remote command execution;
wenzelm
parents: 64128
diff changeset
    93
64131
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
    94
  class Exec private[SSH](
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
    95
    session: Session, kind: String, channel_options: Options, channel: ChannelExec)
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
    96
    extends Channel[ChannelExec](session, kind, channel_options, channel)
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
    97
  {
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
    98
    def kill(signal: String) { channel.sendSignal(signal) }
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
    99
  }
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
   100
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
   101
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
   102
  class Sftp private[SSH](
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
   103
    session: Session, kind: String, channel_options: Options, channel: ChannelSftp)
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
   104
    extends Channel[ChannelSftp](session, kind, channel_options, channel)
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
   105
  {
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
   106
    def home: String = channel.getHome()
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
   107
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
   108
    def chmod(permissions: Int, remote_path: String) { channel.chmod(permissions, remote_path) }
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
   109
    def mv(remote_path1: String, remote_path2: String): Unit =
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
   110
      channel.rename(remote_path1, remote_path2)
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
   111
    def rm(remote_path: String) { channel.rm(remote_path) }
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
   112
    def mkdir(remote_path: String) { channel.mkdir(remote_path) }
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
   113
    def rmdir(remote_path: String) { channel.rmdir(remote_path) }
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
   114
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
   115
    def open_input(remote_path: String): InputStream = channel.get(remote_path)
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
   116
    def open_output(remote_path: String): OutputStream = channel.put(remote_path)
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
   117
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
   118
    def read_file(remote_path: String, local_path: Path): Unit =
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
   119
      channel.get(remote_path, File.platform_path(local_path))
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
   120
    def read_bytes(remote_path: String): Bytes =
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
   121
      using(open_input(remote_path))(Bytes.read_stream(_))
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
   122
    def read(remote_path: String): String =
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
   123
      using(open_input(remote_path))(File.read_stream(_))
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
   124
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
   125
    def write_file(remote_path: String, local_path: Path): Unit =
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
   126
      channel.put(File.platform_path(local_path), remote_path)
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
   127
    def write_bytes(remote_path: String, bytes: Bytes): Unit =
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
   128
      using(open_output(remote_path))(bytes.write_stream(_))
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
   129
    def write(remote_path: String, text: String): Unit =
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
   130
      using(open_output(remote_path))(stream => Bytes(text).write_stream(stream))
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
   131
  }
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
   132
64129
fce8b7c746b4 support for remote command execution;
wenzelm
parents: 64128
diff changeset
   133
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   134
  /* session */
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   135
64130
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
   136
  class Session private[SSH](val session_options: Options, val session: JSch_Session)
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   137
  {
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   138
    override def toString: String =
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   139
      (if (session.getUserName == null) "" else session.getUserName + "@") +
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   140
      (if (session.getHost == null) "" else session.getHost) +
64126
42bcd207598d connect session by default;
wenzelm
parents: 64125
diff changeset
   141
      (if (session.getPort == 22) "" else ":" + session.getPort) +
42bcd207598d connect session by default;
wenzelm
parents: 64125
diff changeset
   142
      (if (session.isConnected) "" else " (disconnected)")
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   143
64126
42bcd207598d connect session by default;
wenzelm
parents: 64125
diff changeset
   144
    def close { session.disconnect }
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   145
64131
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
   146
    def exec(command: String, options: Options = session_options): Exec =
64129
fce8b7c746b4 support for remote command execution;
wenzelm
parents: 64128
diff changeset
   147
    {
64130
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
   148
      val kind = "exec"
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
   149
      val channel = session.openChannel(kind).asInstanceOf[ChannelExec]
64129
fce8b7c746b4 support for remote command execution;
wenzelm
parents: 64128
diff changeset
   150
      channel.setCommand(command)
fce8b7c746b4 support for remote command execution;
wenzelm
parents: 64128
diff changeset
   151
64130
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
   152
      channel.connect(connect_timeout(options))
64131
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
   153
      new Exec(this, kind, options, channel)
64129
fce8b7c746b4 support for remote command execution;
wenzelm
parents: 64128
diff changeset
   154
    }
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   155
64131
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
   156
    def sftp(options: Options = session_options): Sftp =
64130
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
   157
    {
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
   158
      val kind = "sftp"
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
   159
      val channel = session.openChannel(kind).asInstanceOf[ChannelSftp]
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
   160
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
   161
      channel.connect(connect_timeout(options))
64131
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
   162
      new Sftp(this, kind, options, channel)
64130
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
   163
    }
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   164
  }
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   165
}
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   166
64130
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
   167
class SSH private(val options: Options, val jsch: JSch)
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   168
{
64130
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
   169
  def open_session(host: String, port: Int = 22, user: String = null): SSH.Session =
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   170
  {
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   171
    val session = jsch.getSession(user, host, port)
64125
a034dac5ca3c clarified (hardwired!) default (see also jEdit/FTP);
wenzelm
parents: 64124
diff changeset
   172
a034dac5ca3c clarified (hardwired!) default (see also jEdit/FTP);
wenzelm
parents: 64124
diff changeset
   173
    session.setUserInfo(SSH.No_User_Info)
a034dac5ca3c clarified (hardwired!) default (see also jEdit/FTP);
wenzelm
parents: 64124
diff changeset
   174
    session.setConfig("MaxAuthTries", "3")
a034dac5ca3c clarified (hardwired!) default (see also jEdit/FTP);
wenzelm
parents: 64124
diff changeset
   175
64130
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
   176
    if (options.bool("ssh_compression")) {
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   177
      session.setConfig("compression.s2c", "zlib@openssh.com,zlib,none")
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   178
      session.setConfig("compression.c2s", "zlib@openssh.com,zlib,none")
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   179
      session.setConfig("compression_level", "9")
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   180
    }
64125
a034dac5ca3c clarified (hardwired!) default (see also jEdit/FTP);
wenzelm
parents: 64124
diff changeset
   181
64130
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
   182
    session.connect(SSH.connect_timeout(options))
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
   183
    new SSH.Session(options, session)
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   184
  }
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   185
}