src/Pure/General/ssh.scala
author wenzelm
Tue, 06 Mar 2018 15:51:34 +0100
changeset 67770 25f3a278df3d
parent 67745 d83efbe52438
child 67771 3b91c21dcb00
permissions -rw-r--r--
support for permissive connections, for odd situations where host keys are not accepted;
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
64134
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
    10
import java.io.{InputStream, OutputStream, ByteArrayOutputStream}
64131
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
    11
64134
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
    12
import scala.collection.{mutable, JavaConversions}
64131
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
    13
64222
184e3a932778 clarified signature;
wenzelm
parents: 64191
diff changeset
    14
import com.jcraft.jsch.{JSch, Logger => JSch_Logger, Session => JSch_Session, SftpException,
64132
c2594513687b more Sftp operations;
wenzelm
parents: 64131
diff changeset
    15
  OpenSSHConfig, UserInfo, Channel => JSch_Channel, ChannelExec, ChannelSftp, SftpATTRS}
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
{
64185
wenzelm
parents: 64166
diff changeset
    20
  /* target machine: user@host syntax */
64141
79cd4be708fb support user@host syntax;
wenzelm
parents: 64137
diff changeset
    21
64185
wenzelm
parents: 64166
diff changeset
    22
  object Target
64141
79cd4be708fb support user@host syntax;
wenzelm
parents: 64137
diff changeset
    23
  {
79cd4be708fb support user@host syntax;
wenzelm
parents: 64137
diff changeset
    24
    val Pattern = "^([^@]+)@(.+)$".r
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 {
79cd4be708fb support user@host syntax;
wenzelm
parents: 64137
diff changeset
    28
        case Pattern(user, host) => (user, host)
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
64257
9d51ac055cec tuned signature;
wenzelm
parents: 64256
diff changeset
    42
  def connect_timeout(options: Options): Int =
9d51ac055cec tuned signature;
wenzelm
parents: 64256
diff changeset
    43
    options.seconds("ssh_connect_timeout").ms.toInt
64141
79cd4be708fb support user@host syntax;
wenzelm
parents: 64137
diff changeset
    44
64325
47e03cb99274 prevent sporadic disconnection;
wenzelm
parents: 64306
diff changeset
    45
  def alive_interval(options: Options): Int =
47e03cb99274 prevent sporadic disconnection;
wenzelm
parents: 64306
diff changeset
    46
    options.seconds("ssh_alive_interval").ms.toInt
47e03cb99274 prevent sporadic disconnection;
wenzelm
parents: 64306
diff changeset
    47
67273
c573cfb2c407 more robust connection: prefer ServerAliveCountMax=3 (ssh default) instead of 1 (jsch default);
wenzelm
parents: 67067
diff changeset
    48
  def alive_count_max(options: Options): Int =
c573cfb2c407 more robust connection: prefer ServerAliveCountMax=3 (ssh default) instead of 1 (jsch default);
wenzelm
parents: 67067
diff changeset
    49
    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
    50
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    51
64257
9d51ac055cec tuned signature;
wenzelm
parents: 64256
diff changeset
    52
  /* init context */
9d51ac055cec tuned signature;
wenzelm
parents: 64256
diff changeset
    53
9d51ac055cec tuned signature;
wenzelm
parents: 64256
diff changeset
    54
  def init_context(options: Options): Context =
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    55
  {
64130
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
    56
    val config_dir = Path.explode(options.string("ssh_config_dir"))
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    57
    if (!config_dir.is_dir) error("Bad ssh config directory: " + config_dir)
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    58
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    59
    val jsch = new JSch
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    60
64130
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
    61
    val config_file = Path.explode(options.string("ssh_config_file"))
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    62
    if (config_file.is_file)
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    63
      jsch.setConfigRepository(OpenSSHConfig.parseFile(File.platform_path(config_file)))
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    64
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    65
    val known_hosts = config_dir + Path.explode("known_hosts")
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    66
    if (!known_hosts.is_file) known_hosts.file.createNewFile
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    67
    jsch.setKnownHosts(File.platform_path(known_hosts))
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    68
64130
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
    69
    val identity_files =
66923
wenzelm
parents: 66570
diff changeset
    70
      space_explode(':', options.string("ssh_identity_files")).map(Path.explode(_))
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    71
    for (identity_file <- identity_files if identity_file.is_file)
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    72
      jsch.addIdentity(File.platform_path(identity_file))
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    73
64257
9d51ac055cec tuned signature;
wenzelm
parents: 64256
diff changeset
    74
    new Context(options, jsch)
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    75
  }
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    76
67745
d83efbe52438 support for proxy connection, similar to ProxyCommand in ssh config;
wenzelm
parents: 67273
diff changeset
    77
  def open_session(options: Options, host: String, user: String = "", port: Int = 0,
d83efbe52438 support for proxy connection, similar to ProxyCommand in ssh config;
wenzelm
parents: 67273
diff changeset
    78
      proxy_host: String = "", proxy_user: String = "", proxy_port: Int = 0): Session =
d83efbe52438 support for proxy connection, similar to ProxyCommand in ssh config;
wenzelm
parents: 67273
diff changeset
    79
    init_context(options).open_session(host = host, user = user, port = port,
d83efbe52438 support for proxy connection, similar to ProxyCommand in ssh config;
wenzelm
parents: 67273
diff changeset
    80
      proxy_host = proxy_host, proxy_user = proxy_user, proxy_port = proxy_port)
67067
02729ced9b1e tuned signature;
wenzelm
parents: 67066
diff changeset
    81
64257
9d51ac055cec tuned signature;
wenzelm
parents: 64256
diff changeset
    82
  class Context private[SSH](val options: Options, val jsch: JSch)
9d51ac055cec tuned signature;
wenzelm
parents: 64256
diff changeset
    83
  {
9d51ac055cec tuned signature;
wenzelm
parents: 64256
diff changeset
    84
    def update_options(new_options: Options): Context = new Context(new_options, jsch)
9d51ac055cec tuned signature;
wenzelm
parents: 64256
diff changeset
    85
67745
d83efbe52438 support for proxy connection, similar to ProxyCommand in ssh config;
wenzelm
parents: 67273
diff changeset
    86
    def connect_session(host: String, user: String = "", port: Int = 0,
67770
25f3a278df3d support for permissive connections, for odd situations where host keys are not accepted;
wenzelm
parents: 67745
diff changeset
    87
      host_key_permissive: Boolean = false,
25f3a278df3d support for permissive connections, for odd situations where host keys are not accepted;
wenzelm
parents: 67745
diff changeset
    88
      host_key_alias: String = "",
25f3a278df3d support for permissive connections, for odd situations where host keys are not accepted;
wenzelm
parents: 67745
diff changeset
    89
      on_close: () => Unit = () => ()): Session =
64257
9d51ac055cec tuned signature;
wenzelm
parents: 64256
diff changeset
    90
    {
67745
d83efbe52438 support for proxy connection, similar to ProxyCommand in ssh config;
wenzelm
parents: 67273
diff changeset
    91
      val session = jsch.getSession(proper_string(user) getOrElse null, host, make_port(port))
64257
9d51ac055cec tuned signature;
wenzelm
parents: 64256
diff changeset
    92
9d51ac055cec tuned signature;
wenzelm
parents: 64256
diff changeset
    93
      session.setUserInfo(No_User_Info)
64325
47e03cb99274 prevent sporadic disconnection;
wenzelm
parents: 64306
diff changeset
    94
      session.setServerAliveInterval(alive_interval(options))
67273
c573cfb2c407 more robust connection: prefer ServerAliveCountMax=3 (ssh default) instead of 1 (jsch default);
wenzelm
parents: 67067
diff changeset
    95
      session.setServerAliveCountMax(alive_count_max(options))
64257
9d51ac055cec tuned signature;
wenzelm
parents: 64256
diff changeset
    96
      session.setConfig("MaxAuthTries", "3")
67770
25f3a278df3d support for permissive connections, for odd situations where host keys are not accepted;
wenzelm
parents: 67745
diff changeset
    97
      if (host_key_permissive) session.setConfig("StrictHostKeyChecking", "no")
67745
d83efbe52438 support for proxy connection, similar to ProxyCommand in ssh config;
wenzelm
parents: 67273
diff changeset
    98
      if (host_key_alias != "") session.setHostKeyAlias(host_key_alias)
64257
9d51ac055cec tuned signature;
wenzelm
parents: 64256
diff changeset
    99
9d51ac055cec tuned signature;
wenzelm
parents: 64256
diff changeset
   100
      if (options.bool("ssh_compression")) {
9d51ac055cec tuned signature;
wenzelm
parents: 64256
diff changeset
   101
        session.setConfig("compression.s2c", "zlib@openssh.com,zlib,none")
9d51ac055cec tuned signature;
wenzelm
parents: 64256
diff changeset
   102
        session.setConfig("compression.c2s", "zlib@openssh.com,zlib,none")
9d51ac055cec tuned signature;
wenzelm
parents: 64256
diff changeset
   103
        session.setConfig("compression_level", "9")
9d51ac055cec tuned signature;
wenzelm
parents: 64256
diff changeset
   104
      }
67745
d83efbe52438 support for proxy connection, similar to ProxyCommand in ssh config;
wenzelm
parents: 67273
diff changeset
   105
      session.connect(connect_timeout(options))
d83efbe52438 support for proxy connection, similar to ProxyCommand in ssh config;
wenzelm
parents: 67273
diff changeset
   106
      new Session(options, session, on_close)
d83efbe52438 support for proxy connection, similar to ProxyCommand in ssh config;
wenzelm
parents: 67273
diff changeset
   107
    }
64257
9d51ac055cec tuned signature;
wenzelm
parents: 64256
diff changeset
   108
67745
d83efbe52438 support for proxy connection, similar to ProxyCommand in ssh config;
wenzelm
parents: 67273
diff changeset
   109
    def open_session(host: String, user: String = "", port: Int = 0,
67770
25f3a278df3d support for permissive connections, for odd situations where host keys are not accepted;
wenzelm
parents: 67745
diff changeset
   110
      proxy_host: String = "", proxy_user: String = "", proxy_port: Int = 0,
25f3a278df3d support for permissive connections, for odd situations where host keys are not accepted;
wenzelm
parents: 67745
diff changeset
   111
      permissive: Boolean = false): Session =
67745
d83efbe52438 support for proxy connection, similar to ProxyCommand in ssh config;
wenzelm
parents: 67273
diff changeset
   112
    {
d83efbe52438 support for proxy connection, similar to ProxyCommand in ssh config;
wenzelm
parents: 67273
diff changeset
   113
      if (proxy_host == "") connect_session(host = host, user = user, port = port)
d83efbe52438 support for proxy connection, similar to ProxyCommand in ssh config;
wenzelm
parents: 67273
diff changeset
   114
      else {
d83efbe52438 support for proxy connection, similar to ProxyCommand in ssh config;
wenzelm
parents: 67273
diff changeset
   115
        val proxy = connect_session(host = proxy_host, port = proxy_port, user = proxy_user)
d83efbe52438 support for proxy connection, similar to ProxyCommand in ssh config;
wenzelm
parents: 67273
diff changeset
   116
d83efbe52438 support for proxy connection, similar to ProxyCommand in ssh config;
wenzelm
parents: 67273
diff changeset
   117
        val fw =
d83efbe52438 support for proxy connection, similar to ProxyCommand in ssh config;
wenzelm
parents: 67273
diff changeset
   118
          try { proxy.port_forwarding(remote_host = host, remote_port = make_port(port)) }
d83efbe52438 support for proxy connection, similar to ProxyCommand in ssh config;
wenzelm
parents: 67273
diff changeset
   119
          catch { case exn: Throwable => proxy.close; throw exn }
d83efbe52438 support for proxy connection, similar to ProxyCommand in ssh config;
wenzelm
parents: 67273
diff changeset
   120
d83efbe52438 support for proxy connection, similar to ProxyCommand in ssh config;
wenzelm
parents: 67273
diff changeset
   121
        try {
67770
25f3a278df3d support for permissive connections, for odd situations where host keys are not accepted;
wenzelm
parents: 67745
diff changeset
   122
          connect_session(host = fw.local_host, port = fw.local_port,
25f3a278df3d support for permissive connections, for odd situations where host keys are not accepted;
wenzelm
parents: 67745
diff changeset
   123
            host_key_permissive = permissive, host_key_alias = host,
67745
d83efbe52438 support for proxy connection, similar to ProxyCommand in ssh config;
wenzelm
parents: 67273
diff changeset
   124
            user = user, on_close = () => { fw.close; proxy.close })
d83efbe52438 support for proxy connection, similar to ProxyCommand in ssh config;
wenzelm
parents: 67273
diff changeset
   125
        }
d83efbe52438 support for proxy connection, similar to ProxyCommand in ssh config;
wenzelm
parents: 67273
diff changeset
   126
        catch { case exn: Throwable => fw.close; proxy.close; throw exn }
d83efbe52438 support for proxy connection, similar to ProxyCommand in ssh config;
wenzelm
parents: 67273
diff changeset
   127
      }
64257
9d51ac055cec tuned signature;
wenzelm
parents: 64256
diff changeset
   128
    }
9d51ac055cec tuned signature;
wenzelm
parents: 64256
diff changeset
   129
  }
64130
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
   130
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   131
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   132
  /* logging */
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   133
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   134
  def logging(verbose: Boolean = true, debug: Boolean = false)
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   135
  {
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   136
    JSch.setLogger(if (verbose) new Logger(debug) else null)
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   137
  }
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   138
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   139
  private class Logger(debug: Boolean) extends JSch_Logger
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   140
  {
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   141
    def isEnabled(level: Int): Boolean = level != JSch_Logger.DEBUG || debug
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   142
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   143
    def log(level: Int, msg: String)
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   144
    {
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   145
      level match {
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   146
        case JSch_Logger.ERROR | JSch_Logger.FATAL => Output.error_message(msg)
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   147
        case JSch_Logger.WARN => Output.warning(msg)
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   148
        case _ => Output.writeln(msg)
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   149
      }
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   150
    }
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   151
  }
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   152
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   153
64128
wenzelm
parents: 64127
diff changeset
   154
  /* user info */
wenzelm
parents: 64127
diff changeset
   155
wenzelm
parents: 64127
diff changeset
   156
  object No_User_Info extends UserInfo
wenzelm
parents: 64127
diff changeset
   157
  {
wenzelm
parents: 64127
diff changeset
   158
    def getPassphrase: String = null
wenzelm
parents: 64127
diff changeset
   159
    def getPassword: String = null
wenzelm
parents: 64127
diff changeset
   160
    def promptPassword(msg: String): Boolean = false
wenzelm
parents: 64127
diff changeset
   161
    def promptPassphrase(msg: String): Boolean = false
wenzelm
parents: 64127
diff changeset
   162
    def promptYesNo(msg: String): Boolean = false
wenzelm
parents: 64127
diff changeset
   163
    def showMessage(msg: String): Unit = Output.writeln(msg)
wenzelm
parents: 64127
diff changeset
   164
  }
wenzelm
parents: 64127
diff changeset
   165
wenzelm
parents: 64127
diff changeset
   166
65009
eda9366bbfac remote database access via ssh port forwarding;
wenzelm
parents: 64347
diff changeset
   167
  /* port forwarding */
eda9366bbfac remote database access via ssh port forwarding;
wenzelm
parents: 64347
diff changeset
   168
65010
a27e9908dcf7 clarified signature;
wenzelm
parents: 65009
diff changeset
   169
  object Port_Forwarding
65009
eda9366bbfac remote database access via ssh port forwarding;
wenzelm
parents: 64347
diff changeset
   170
  {
65636
df804cdba5f9 ssh_close for proper termination after use of database;
wenzelm
parents: 65594
diff changeset
   171
    def open(ssh: Session, ssh_close: Boolean,
65010
a27e9908dcf7 clarified signature;
wenzelm
parents: 65009
diff changeset
   172
      local_host: String, local_port: Int, remote_host: String, remote_port: Int): Port_Forwarding =
a27e9908dcf7 clarified signature;
wenzelm
parents: 65009
diff changeset
   173
    {
a27e9908dcf7 clarified signature;
wenzelm
parents: 65009
diff changeset
   174
      val port = ssh.session.setPortForwardingL(local_host, local_port, remote_host, remote_port)
65636
df804cdba5f9 ssh_close for proper termination after use of database;
wenzelm
parents: 65594
diff changeset
   175
      new Port_Forwarding(ssh, ssh_close, local_host, port, remote_host, remote_port)
65010
a27e9908dcf7 clarified signature;
wenzelm
parents: 65009
diff changeset
   176
    }
a27e9908dcf7 clarified signature;
wenzelm
parents: 65009
diff changeset
   177
  }
a27e9908dcf7 clarified signature;
wenzelm
parents: 65009
diff changeset
   178
a27e9908dcf7 clarified signature;
wenzelm
parents: 65009
diff changeset
   179
  class Port_Forwarding private[SSH](
a27e9908dcf7 clarified signature;
wenzelm
parents: 65009
diff changeset
   180
    ssh: SSH.Session,
65636
df804cdba5f9 ssh_close for proper termination after use of database;
wenzelm
parents: 65594
diff changeset
   181
    ssh_close: Boolean,
65010
a27e9908dcf7 clarified signature;
wenzelm
parents: 65009
diff changeset
   182
    val local_host: String,
a27e9908dcf7 clarified signature;
wenzelm
parents: 65009
diff changeset
   183
    val local_port: Int,
a27e9908dcf7 clarified signature;
wenzelm
parents: 65009
diff changeset
   184
    val remote_host: String,
a27e9908dcf7 clarified signature;
wenzelm
parents: 65009
diff changeset
   185
    val remote_port: Int)
a27e9908dcf7 clarified signature;
wenzelm
parents: 65009
diff changeset
   186
  {
a27e9908dcf7 clarified signature;
wenzelm
parents: 65009
diff changeset
   187
    override def toString: String =
a27e9908dcf7 clarified signature;
wenzelm
parents: 65009
diff changeset
   188
      local_host + ":" + local_port + ":" + remote_host + ":" + remote_port
a27e9908dcf7 clarified signature;
wenzelm
parents: 65009
diff changeset
   189
65636
df804cdba5f9 ssh_close for proper termination after use of database;
wenzelm
parents: 65594
diff changeset
   190
    def close()
df804cdba5f9 ssh_close for proper termination after use of database;
wenzelm
parents: 65594
diff changeset
   191
    {
df804cdba5f9 ssh_close for proper termination after use of database;
wenzelm
parents: 65594
diff changeset
   192
      ssh.session.delPortForwardingL(local_host, local_port)
df804cdba5f9 ssh_close for proper termination after use of database;
wenzelm
parents: 65594
diff changeset
   193
      if (ssh_close) ssh.close()
df804cdba5f9 ssh_close for proper termination after use of database;
wenzelm
parents: 65594
diff changeset
   194
    }
65009
eda9366bbfac remote database access via ssh port forwarding;
wenzelm
parents: 64347
diff changeset
   195
  }
eda9366bbfac remote database access via ssh port forwarding;
wenzelm
parents: 64347
diff changeset
   196
eda9366bbfac remote database access via ssh port forwarding;
wenzelm
parents: 64347
diff changeset
   197
64191
wenzelm
parents: 64190
diff changeset
   198
  /* Sftp channel */
wenzelm
parents: 64190
diff changeset
   199
wenzelm
parents: 64190
diff changeset
   200
  type Attrs = SftpATTRS
wenzelm
parents: 64190
diff changeset
   201
64233
ef6f7e8a018c clarified signature: more static types;
wenzelm
parents: 64228
diff changeset
   202
  sealed case class Dir_Entry(name: Path, attrs: Attrs)
64191
wenzelm
parents: 64190
diff changeset
   203
  {
wenzelm
parents: 64190
diff changeset
   204
    def is_file: Boolean = attrs.isReg
wenzelm
parents: 64190
diff changeset
   205
    def is_dir: Boolean = attrs.isDir
wenzelm
parents: 64190
diff changeset
   206
  }
wenzelm
parents: 64190
diff changeset
   207
wenzelm
parents: 64190
diff changeset
   208
64132
c2594513687b more Sftp operations;
wenzelm
parents: 64131
diff changeset
   209
  /* exec channel */
c2594513687b more Sftp operations;
wenzelm
parents: 64131
diff changeset
   210
64134
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   211
  private val exec_wait_delay = Time.seconds(0.3)
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   212
64256
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   213
  class Exec private[SSH](session: Session, channel: ChannelExec)
64131
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
   214
  {
64256
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   215
    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
   216
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   217
    def close() { channel.disconnect }
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   218
64134
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   219
    val exit_status: Future[Int] =
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   220
      Future.thread("ssh_wait") {
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   221
        while (!channel.isClosed) Thread.sleep(exec_wait_delay.ms)
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   222
        channel.getExitStatus
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   223
      }
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   224
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   225
    val stdin: OutputStream = channel.getOutputStream
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   226
    val stdout: InputStream = channel.getInputStream
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   227
    val stderr: InputStream = channel.getErrStream
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   228
64166
44925cf6ded1 tuned signature;
wenzelm
parents: 64142
diff changeset
   229
    // connect after preparing streams
44925cf6ded1 tuned signature;
wenzelm
parents: 64142
diff changeset
   230
    channel.connect(connect_timeout(session.options))
64134
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   231
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   232
    def result(
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   233
      progress_stdout: String => Unit = (_: String) => (),
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   234
      progress_stderr: String => Unit = (_: String) => (),
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   235
      strict: Boolean = true): Process_Result =
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
      stdin.close
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   238
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   239
      def read_lines(stream: InputStream, progress: String => Unit): List[String] =
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   240
      {
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   241
        val result = new mutable.ListBuffer[String]
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   242
        val line_buffer = new ByteArrayOutputStream(100)
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   243
        def line_flush()
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   244
        {
64326
ff3c383b9163 extra trim_line for the sake of Windows;
wenzelm
parents: 64325
diff changeset
   245
          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
   246
          progress(line)
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   247
          result += line
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   248
          line_buffer.reset
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
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   251
        var c = 0
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   252
        var finished = false
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   253
        while (!finished) {
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   254
          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
   255
          if (c == 10) line_flush()
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   256
          else if (channel.isClosed) {
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   257
            if (line_buffer.size > 0) line_flush()
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   258
            finished = true
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   259
          }
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   260
          else Thread.sleep(exec_wait_delay.ms)
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
        result.toList
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   264
      }
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   265
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   266
      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
   267
      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
   268
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   269
      def terminate()
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   270
      {
64136
7c5191489457 close more thoroughly;
wenzelm
parents: 64135
diff changeset
   271
        close
64134
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   272
        out_lines.join
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   273
        err_lines.join
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   274
        exit_status.join
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   275
      }
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   276
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   277
      val rc =
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   278
        try { exit_status.join }
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   279
        catch { case Exn.Interrupt() => terminate(); Exn.Interrupt.return_code }
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   280
64136
7c5191489457 close more thoroughly;
wenzelm
parents: 64135
diff changeset
   281
      close
64134
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   282
      if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   283
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   284
      Process_Result(rc, out_lines.join, err_lines.join)
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   285
    }
64131
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
   286
  }
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
   287
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
   288
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   289
  /* session */
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   290
67745
d83efbe52438 support for proxy connection, similar to ProxyCommand in ssh config;
wenzelm
parents: 67273
diff changeset
   291
  class Session private[SSH](
d83efbe52438 support for proxy connection, similar to ProxyCommand in ssh config;
wenzelm
parents: 67273
diff changeset
   292
    val options: Options,
d83efbe52438 support for proxy connection, similar to ProxyCommand in ssh config;
wenzelm
parents: 67273
diff changeset
   293
    val session: JSch_Session,
d83efbe52438 support for proxy connection, similar to ProxyCommand in ssh config;
wenzelm
parents: 67273
diff changeset
   294
    on_close: () => Unit) extends System
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   295
  {
67745
d83efbe52438 support for proxy connection, similar to ProxyCommand in ssh config;
wenzelm
parents: 67273
diff changeset
   296
    def update_options(new_options: Options): Session =
d83efbe52438 support for proxy connection, similar to ProxyCommand in ssh config;
wenzelm
parents: 67273
diff changeset
   297
      new Session(new_options, session, on_close)
64166
44925cf6ded1 tuned signature;
wenzelm
parents: 64142
diff changeset
   298
64347
602483aa7818 support for URL notation;
wenzelm
parents: 64326
diff changeset
   299
    def user_prefix: String = if (session.getUserName == null) "" else session.getUserName + "@"
602483aa7818 support for URL notation;
wenzelm
parents: 64326
diff changeset
   300
    def host: String = if (session.getHost == null) "" else session.getHost
602483aa7818 support for URL notation;
wenzelm
parents: 64326
diff changeset
   301
    def port_suffix: String = if (session.getPort == default_port) "" else ":" + session.getPort
66570
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   302
    override def hg_url: String = "ssh://" + user_prefix + host + port_suffix + "/"
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   303
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   304
    override def prefix: String =
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   305
      user_prefix + host + port_suffix + ":"
64347
602483aa7818 support for URL notation;
wenzelm
parents: 64326
diff changeset
   306
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   307
    override def toString: String =
64347
602483aa7818 support for URL notation;
wenzelm
parents: 64326
diff changeset
   308
      user_prefix + host + port_suffix + (if (session.isConnected) "" else " (disconnected)")
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   309
64256
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   310
65009
eda9366bbfac remote database access via ssh port forwarding;
wenzelm
parents: 64347
diff changeset
   311
    /* port forwarding */
eda9366bbfac remote database access via ssh port forwarding;
wenzelm
parents: 64347
diff changeset
   312
65636
df804cdba5f9 ssh_close for proper termination after use of database;
wenzelm
parents: 65594
diff changeset
   313
    def port_forwarding(
df804cdba5f9 ssh_close for proper termination after use of database;
wenzelm
parents: 65594
diff changeset
   314
        remote_port: Int, remote_host: String = "localhost",
df804cdba5f9 ssh_close for proper termination after use of database;
wenzelm
parents: 65594
diff changeset
   315
        local_port: Int = 0, local_host: String = "localhost",
df804cdba5f9 ssh_close for proper termination after use of database;
wenzelm
parents: 65594
diff changeset
   316
        ssh_close: Boolean = false): Port_Forwarding =
df804cdba5f9 ssh_close for proper termination after use of database;
wenzelm
parents: 65594
diff changeset
   317
      Port_Forwarding.open(this, ssh_close, local_host, local_port, remote_host, remote_port)
65009
eda9366bbfac remote database access via ssh port forwarding;
wenzelm
parents: 64347
diff changeset
   318
eda9366bbfac remote database access via ssh port forwarding;
wenzelm
parents: 64347
diff changeset
   319
64256
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   320
    /* sftp channel */
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   321
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   322
    val sftp: ChannelSftp = session.openChannel("sftp").asInstanceOf[ChannelSftp]
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   323
    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
   324
67745
d83efbe52438 support for proxy connection, similar to ProxyCommand in ssh config;
wenzelm
parents: 67273
diff changeset
   325
    def close() { sftp.disconnect; session.disconnect; on_close() }
64256
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   326
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   327
    val settings: Map[String, String] =
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   328
    {
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   329
      val home = sftp.getHome
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   330
      Map("HOME" -> home, "USER_HOME" -> home)
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   331
    }
66570
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   332
    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
   333
    def remote_path(path: Path): String = expand_path(path).implode
67066
1645cef7a49c proper ssh.bash_path;
wenzelm
parents: 66923
diff changeset
   334
    override def bash_path(path: Path): String = Bash.string(remote_path(path))
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   335
64256
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   336
    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
   337
    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
   338
    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
   339
    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
   340
    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
   341
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   342
    def stat(path: Path): Option[Dir_Entry] =
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   343
      try { Some(Dir_Entry(expand_path(path), sftp.stat(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
   344
      catch { case _: SftpException => None }
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   345
66570
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   346
    override def is_file(path: Path): Boolean = stat(path).map(_.is_file) getOrElse false
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   347
    override def is_dir(path: Path): Boolean = stat(path).map(_.is_dir) getOrElse false
64256
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   348
66570
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   349
    override def mkdirs(path: Path): Unit =
64256
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   350
      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
   351
        execute(
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   352
          "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
   353
        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
   354
      }
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   355
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   356
    def read_dir(path: Path): List[Dir_Entry] =
64191
wenzelm
parents: 64190
diff changeset
   357
    {
64256
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   358
      val dir = sftp.ls(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
      (for {
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   360
        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
   361
        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
   362
        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
   363
        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
   364
        if name != "." && name != ".."
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   365
      } yield Dir_Entry(Path.basic(name), attrs)).toList
64191
wenzelm
parents: 64190
diff changeset
   366
    }
64135
865dda40e1cc provide execute operation, similar to Isabelle_System.bash;
wenzelm
parents: 64134
diff changeset
   367
64256
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   368
    def find_files(root: Path, pred: Dir_Entry => Boolean = _ => true): List[Dir_Entry] =
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   369
    {
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   370
      def find(dir: Path): List[Dir_Entry] =
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   371
        read_dir(dir).flatMap(entry =>
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   372
          {
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   373
            val file = dir + entry.name
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   374
            if (entry.is_dir) find(file)
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   375
            else if (pred(entry)) List(entry.copy(name = file))
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   376
            else Nil
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   377
          })
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   378
      find(root)
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   379
    }
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   380
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   381
    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
   382
    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
   383
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   384
    def read_file(path: Path, local_path: Path): Unit =
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   385
      sftp.get(remote_path(path), File.platform_path(local_path))
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   386
    def read_bytes(path: Path): Bytes = using(open_input(path))(Bytes.read_stream(_))
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   387
    def read(path: Path): String = using(open_input(path))(File.read_stream(_))
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   388
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   389
    def write_file(path: Path, local_path: Path): Unit =
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   390
      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
   391
    def write_bytes(path: Path, bytes: Bytes): Unit =
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   392
      using(open_output(path))(bytes.write_stream(_))
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   393
    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
   394
      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
   395
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   396
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   397
    /* exec channel */
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   398
64166
44925cf6ded1 tuned signature;
wenzelm
parents: 64142
diff changeset
   399
    def exec(command: String): Exec =
64129
fce8b7c746b4 support for remote command execution;
wenzelm
parents: 64128
diff changeset
   400
    {
64256
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   401
      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
   402
      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
   403
      new Exec(this, channel)
64129
fce8b7c746b4 support for remote command execution;
wenzelm
parents: 64128
diff changeset
   404
    }
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   405
66570
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   406
    override def execute(command: String,
64191
wenzelm
parents: 64190
diff changeset
   407
        progress_stdout: String => Unit = (_: String) => (),
wenzelm
parents: 64190
diff changeset
   408
        progress_stderr: String => Unit = (_: String) => (),
wenzelm
parents: 64190
diff changeset
   409
        strict: Boolean = true): Process_Result =
wenzelm
parents: 64190
diff changeset
   410
      exec(command).result(progress_stdout, progress_stderr, strict)
64137
e9b3d9c1bc5a support for remote tmp dirs;
wenzelm
parents: 64136
diff changeset
   411
e9b3d9c1bc5a support for remote tmp dirs;
wenzelm
parents: 64136
diff changeset
   412
e9b3d9c1bc5a support for remote tmp dirs;
wenzelm
parents: 64136
diff changeset
   413
    /* tmp dirs */
e9b3d9c1bc5a support for remote tmp dirs;
wenzelm
parents: 64136
diff changeset
   414
64306
7b6dc1b36f20 tuned signature, in accordance to Isabelle_System;
wenzelm
parents: 64304
diff changeset
   415
    def rm_tree(dir: Path): Unit = rm_tree(remote_path(dir))
7b6dc1b36f20 tuned signature, in accordance to Isabelle_System;
wenzelm
parents: 64304
diff changeset
   416
64137
e9b3d9c1bc5a support for remote tmp dirs;
wenzelm
parents: 64136
diff changeset
   417
    def rm_tree(remote_dir: String): Unit =
64304
96bc94c87a81 clarified modules;
wenzelm
parents: 64258
diff changeset
   418
      execute("rm -r -f " + Bash.string(remote_dir)).check
64137
e9b3d9c1bc5a support for remote tmp dirs;
wenzelm
parents: 64136
diff changeset
   419
e9b3d9c1bc5a support for remote tmp dirs;
wenzelm
parents: 64136
diff changeset
   420
    def tmp_dir(): String =
e9b3d9c1bc5a support for remote tmp dirs;
wenzelm
parents: 64136
diff changeset
   421
      execute("mktemp -d -t tmp.XXXXXXXXXX").check.out
e9b3d9c1bc5a support for remote tmp dirs;
wenzelm
parents: 64136
diff changeset
   422
64233
ef6f7e8a018c clarified signature: more static types;
wenzelm
parents: 64228
diff changeset
   423
    def with_tmp_dir[A](body: Path => A): A =
64137
e9b3d9c1bc5a support for remote tmp dirs;
wenzelm
parents: 64136
diff changeset
   424
    {
e9b3d9c1bc5a support for remote tmp dirs;
wenzelm
parents: 64136
diff changeset
   425
      val remote_dir = tmp_dir()
64233
ef6f7e8a018c clarified signature: more static types;
wenzelm
parents: 64228
diff changeset
   426
      try { body(Path.explode(remote_dir)) } finally { rm_tree(remote_dir) }
64137
e9b3d9c1bc5a support for remote tmp dirs;
wenzelm
parents: 64136
diff changeset
   427
    }
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   428
  }
66570
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   429
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   430
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   431
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   432
  /* system operations */
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   433
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   434
  trait System
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   435
  {
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   436
    def hg_url: String = ""
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   437
    def prefix: String = ""
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   438
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   439
    def expand_path(path: Path): Path = path.expand
67066
1645cef7a49c proper ssh.bash_path;
wenzelm
parents: 66923
diff changeset
   440
    def bash_path(path: Path): String = File.bash_path(path)
66570
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   441
    def is_file(path: Path): Boolean = path.is_file
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   442
    def is_dir(path: Path): Boolean = path.is_dir
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   443
    def mkdirs(path: Path): Unit = Isabelle_System.mkdirs(path)
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   444
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   445
    def execute(command: String,
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   446
        progress_stdout: String => Unit = (_: String) => (),
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   447
        progress_stderr: String => Unit = (_: String) => (),
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   448
        strict: Boolean = true): Process_Result =
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   449
      Isabelle_System.bash(command, progress_stdout = progress_stdout,
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   450
        progress_stderr = progress_stderr, strict = strict)
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   451
  }
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   452
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   453
  object Local extends System
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   454
}