src/Pure/General/ssh.scala
author wenzelm
Thu, 13 Oct 2016 15:41:30 +0200
changeset 64191 1dcb5acd9a71
parent 64190 c62b99e3ec07
child 64222 184e3a932778
permissions -rw-r--r--
tuned;
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
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    14
import com.jcraft.jsch.{JSch, Logger => JSch_Logger, Session => JSch_Session,
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
954451356017 proper type for Library.using;
wenzelm
parents: 64141
diff changeset
    40
64141
79cd4be708fb support user@host syntax;
wenzelm
parents: 64137
diff changeset
    41
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    42
  /* init */
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    43
64130
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
    44
  def init(options: Options): SSH =
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    45
  {
64130
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
    46
    val config_dir = Path.explode(options.string("ssh_config_dir"))
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    47
    if (!config_dir.is_dir) error("Bad ssh config directory: " + config_dir)
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    48
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    49
    val jsch = new JSch
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    50
64130
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
    51
    val config_file = Path.explode(options.string("ssh_config_file"))
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    52
    if (config_file.is_file)
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    53
      jsch.setConfigRepository(OpenSSHConfig.parseFile(File.platform_path(config_file)))
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    54
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    55
    val known_hosts = config_dir + Path.explode("known_hosts")
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    56
    if (!known_hosts.is_file) known_hosts.file.createNewFile
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    57
    jsch.setKnownHosts(File.platform_path(known_hosts))
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    58
64130
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
    59
    val identity_files =
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
    60
      Library.space_explode(':', options.string("ssh_identity_files")).map(Path.explode(_))
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    61
    for (identity_file <- identity_files if identity_file.is_file)
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    62
      jsch.addIdentity(File.platform_path(identity_file))
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    63
64130
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
    64
    new SSH(options, jsch)
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    65
  }
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    66
64130
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
    67
  def connect_timeout(options: Options): Int =
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
    68
    options.seconds("ssh_connect_timeout").ms.toInt
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
    69
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    70
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    71
  /* logging */
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    72
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    73
  def logging(verbose: Boolean = true, debug: Boolean = false)
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    74
  {
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    75
    JSch.setLogger(if (verbose) new Logger(debug) else null)
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    76
  }
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    77
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    78
  private class Logger(debug: Boolean) extends JSch_Logger
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    79
  {
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    80
    def isEnabled(level: Int): Boolean = level != JSch_Logger.DEBUG || debug
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    81
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    82
    def log(level: Int, msg: String)
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    83
    {
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    84
      level match {
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    85
        case JSch_Logger.ERROR | JSch_Logger.FATAL => Output.error_message(msg)
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    86
        case JSch_Logger.WARN => Output.warning(msg)
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    87
        case _ => Output.writeln(msg)
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    88
      }
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    89
    }
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    90
  }
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    91
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    92
64128
wenzelm
parents: 64127
diff changeset
    93
  /* user info */
wenzelm
parents: 64127
diff changeset
    94
wenzelm
parents: 64127
diff changeset
    95
  object No_User_Info extends UserInfo
wenzelm
parents: 64127
diff changeset
    96
  {
wenzelm
parents: 64127
diff changeset
    97
    def getPassphrase: String = null
wenzelm
parents: 64127
diff changeset
    98
    def getPassword: String = null
wenzelm
parents: 64127
diff changeset
    99
    def promptPassword(msg: String): Boolean = false
wenzelm
parents: 64127
diff changeset
   100
    def promptPassphrase(msg: String): Boolean = false
wenzelm
parents: 64127
diff changeset
   101
    def promptYesNo(msg: String): Boolean = false
wenzelm
parents: 64127
diff changeset
   102
    def showMessage(msg: String): Unit = Output.writeln(msg)
wenzelm
parents: 64127
diff changeset
   103
  }
wenzelm
parents: 64127
diff changeset
   104
wenzelm
parents: 64127
diff changeset
   105
64132
c2594513687b more Sftp operations;
wenzelm
parents: 64131
diff changeset
   106
  /* channel */
64129
fce8b7c746b4 support for remote command execution;
wenzelm
parents: 64128
diff changeset
   107
64134
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   108
  class Channel[C <: JSch_Channel] private[SSH](
64166
44925cf6ded1 tuned signature;
wenzelm
parents: 64142
diff changeset
   109
    val session: Session, val kind: String, val channel: C)
64129
fce8b7c746b4 support for remote command execution;
wenzelm
parents: 64128
diff changeset
   110
  {
64130
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
   111
    override def toString: String = kind + " " + session.toString
64129
fce8b7c746b4 support for remote command execution;
wenzelm
parents: 64128
diff changeset
   112
64142
954451356017 proper type for Library.using;
wenzelm
parents: 64141
diff changeset
   113
    def close() { channel.disconnect }
64129
fce8b7c746b4 support for remote command execution;
wenzelm
parents: 64128
diff changeset
   114
  }
fce8b7c746b4 support for remote command execution;
wenzelm
parents: 64128
diff changeset
   115
64132
c2594513687b more Sftp operations;
wenzelm
parents: 64131
diff changeset
   116
64191
wenzelm
parents: 64190
diff changeset
   117
  /* Sftp channel */
wenzelm
parents: 64190
diff changeset
   118
wenzelm
parents: 64190
diff changeset
   119
  type Attrs = SftpATTRS
wenzelm
parents: 64190
diff changeset
   120
wenzelm
parents: 64190
diff changeset
   121
  sealed case class Dir_Entry(name: String, attrs: Attrs)
wenzelm
parents: 64190
diff changeset
   122
  {
wenzelm
parents: 64190
diff changeset
   123
    def is_file: Boolean = attrs.isReg
wenzelm
parents: 64190
diff changeset
   124
    def is_dir: Boolean = attrs.isDir
wenzelm
parents: 64190
diff changeset
   125
  }
wenzelm
parents: 64190
diff changeset
   126
wenzelm
parents: 64190
diff changeset
   127
  class Sftp private[SSH](session: Session, kind: String, channel: ChannelSftp)
wenzelm
parents: 64190
diff changeset
   128
    extends Channel[ChannelSftp](session, kind, channel)
wenzelm
parents: 64190
diff changeset
   129
  {
wenzelm
parents: 64190
diff changeset
   130
    channel.connect(connect_timeout(session.options))
wenzelm
parents: 64190
diff changeset
   131
wenzelm
parents: 64190
diff changeset
   132
    def home: String = channel.getHome()
wenzelm
parents: 64190
diff changeset
   133
wenzelm
parents: 64190
diff changeset
   134
    def chmod(permissions: Int, remote_path: String) { channel.chmod(permissions, remote_path) }
wenzelm
parents: 64190
diff changeset
   135
    def mv(remote_path1: String, remote_path2: String): Unit =
wenzelm
parents: 64190
diff changeset
   136
      channel.rename(remote_path1, remote_path2)
wenzelm
parents: 64190
diff changeset
   137
    def rm(remote_path: String) { channel.rm(remote_path) }
wenzelm
parents: 64190
diff changeset
   138
    def mkdir(remote_path: String) { channel.mkdir(remote_path) }
wenzelm
parents: 64190
diff changeset
   139
    def rmdir(remote_path: String) { channel.rmdir(remote_path) }
wenzelm
parents: 64190
diff changeset
   140
wenzelm
parents: 64190
diff changeset
   141
    def stat(remote_path: String): Dir_Entry =
wenzelm
parents: 64190
diff changeset
   142
      Dir_Entry(remote_path, channel.stat(remote_path))
wenzelm
parents: 64190
diff changeset
   143
wenzelm
parents: 64190
diff changeset
   144
    def read_dir(remote_path: String): List[Dir_Entry] =
wenzelm
parents: 64190
diff changeset
   145
    {
wenzelm
parents: 64190
diff changeset
   146
      val dir = channel.ls(remote_path)
wenzelm
parents: 64190
diff changeset
   147
      (for {
wenzelm
parents: 64190
diff changeset
   148
        i <- (0 until dir.size).iterator
wenzelm
parents: 64190
diff changeset
   149
        a = dir.get(i).asInstanceOf[AnyRef]
wenzelm
parents: 64190
diff changeset
   150
        name = Untyped.get[String](a, "filename")
wenzelm
parents: 64190
diff changeset
   151
        attrs = Untyped.get[Attrs](a, "attrs")
wenzelm
parents: 64190
diff changeset
   152
        if name != "." && name != ".."
wenzelm
parents: 64190
diff changeset
   153
      } yield Dir_Entry(name, attrs)).toList
wenzelm
parents: 64190
diff changeset
   154
    }
wenzelm
parents: 64190
diff changeset
   155
wenzelm
parents: 64190
diff changeset
   156
    def find_files(remote_path: String, pred: Dir_Entry => Boolean = _ => true): List[Dir_Entry] =
wenzelm
parents: 64190
diff changeset
   157
    {
wenzelm
parents: 64190
diff changeset
   158
      def find(dir: String): List[Dir_Entry] =
wenzelm
parents: 64190
diff changeset
   159
        read_dir(dir).flatMap(entry =>
wenzelm
parents: 64190
diff changeset
   160
          {
wenzelm
parents: 64190
diff changeset
   161
            val file = dir + "/" + entry.name
wenzelm
parents: 64190
diff changeset
   162
            if (entry.is_dir) find(file)
wenzelm
parents: 64190
diff changeset
   163
            else if (pred(entry)) List(entry.copy(name = file))
wenzelm
parents: 64190
diff changeset
   164
            else Nil
wenzelm
parents: 64190
diff changeset
   165
          })
wenzelm
parents: 64190
diff changeset
   166
      find(remote_path)
wenzelm
parents: 64190
diff changeset
   167
    }
wenzelm
parents: 64190
diff changeset
   168
wenzelm
parents: 64190
diff changeset
   169
    def open_input(remote_path: String): InputStream = channel.get(remote_path)
wenzelm
parents: 64190
diff changeset
   170
    def open_output(remote_path: String): OutputStream = channel.put(remote_path)
wenzelm
parents: 64190
diff changeset
   171
wenzelm
parents: 64190
diff changeset
   172
    def read_file(remote_path: String, local_path: Path): Unit =
wenzelm
parents: 64190
diff changeset
   173
      channel.get(remote_path, File.platform_path(local_path))
wenzelm
parents: 64190
diff changeset
   174
    def read_bytes(remote_path: String): Bytes =
wenzelm
parents: 64190
diff changeset
   175
      using(open_input(remote_path))(Bytes.read_stream(_))
wenzelm
parents: 64190
diff changeset
   176
    def read(remote_path: String): String =
wenzelm
parents: 64190
diff changeset
   177
      using(open_input(remote_path))(File.read_stream(_))
wenzelm
parents: 64190
diff changeset
   178
wenzelm
parents: 64190
diff changeset
   179
    def write_file(remote_path: String, local_path: Path): Unit =
wenzelm
parents: 64190
diff changeset
   180
      channel.put(File.platform_path(local_path), remote_path)
wenzelm
parents: 64190
diff changeset
   181
    def write_bytes(remote_path: String, bytes: Bytes): Unit =
wenzelm
parents: 64190
diff changeset
   182
      using(open_output(remote_path))(bytes.write_stream(_))
wenzelm
parents: 64190
diff changeset
   183
    def write(remote_path: String, text: String): Unit =
wenzelm
parents: 64190
diff changeset
   184
      using(open_output(remote_path))(stream => Bytes(text).write_stream(stream))
wenzelm
parents: 64190
diff changeset
   185
  }
wenzelm
parents: 64190
diff changeset
   186
wenzelm
parents: 64190
diff changeset
   187
64132
c2594513687b more Sftp operations;
wenzelm
parents: 64131
diff changeset
   188
  /* exec channel */
c2594513687b more Sftp operations;
wenzelm
parents: 64131
diff changeset
   189
64134
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   190
  private val exec_wait_delay = Time.seconds(0.3)
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   191
64166
44925cf6ded1 tuned signature;
wenzelm
parents: 64142
diff changeset
   192
  class Exec private[SSH](session: Session, kind: String, channel: ChannelExec)
44925cf6ded1 tuned signature;
wenzelm
parents: 64142
diff changeset
   193
    extends Channel[ChannelExec](session, kind, channel)
64131
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
   194
  {
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
   195
    def kill(signal: String) { channel.sendSignal(signal) }
64134
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   196
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   197
    val exit_status: Future[Int] =
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   198
      Future.thread("ssh_wait") {
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   199
        while (!channel.isClosed) Thread.sleep(exec_wait_delay.ms)
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   200
        channel.getExitStatus
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   201
      }
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   202
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   203
    val stdin: OutputStream = channel.getOutputStream
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   204
    val stdout: InputStream = channel.getInputStream
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   205
    val stderr: InputStream = channel.getErrStream
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   206
64166
44925cf6ded1 tuned signature;
wenzelm
parents: 64142
diff changeset
   207
    // connect after preparing streams
44925cf6ded1 tuned signature;
wenzelm
parents: 64142
diff changeset
   208
    channel.connect(connect_timeout(session.options))
64134
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   209
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   210
    def result(
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   211
      progress_stdout: String => Unit = (_: String) => (),
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   212
      progress_stderr: String => Unit = (_: String) => (),
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   213
      strict: Boolean = true): Process_Result =
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   214
    {
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   215
      stdin.close
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   216
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   217
      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
   218
      {
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   219
        val result = new mutable.ListBuffer[String]
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   220
        val line_buffer = new ByteArrayOutputStream(100)
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   221
        def line_flush()
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   222
        {
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   223
          val line = line_buffer.toString(UTF8.charset_name)
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   224
          progress(line)
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   225
          result += line
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   226
          line_buffer.reset
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   227
        }
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   228
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   229
        var c = 0
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   230
        var finished = false
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   231
        while (!finished) {
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   232
          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
   233
          if (c == 10) line_flush()
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   234
          else if (channel.isClosed) {
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   235
            if (line_buffer.size > 0) line_flush()
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   236
            finished = true
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
          else Thread.sleep(exec_wait_delay.ms)
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   239
        }
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
        result.toList
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   242
      }
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   243
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   244
      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
   245
      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
   246
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   247
      def terminate()
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   248
      {
64136
7c5191489457 close more thoroughly;
wenzelm
parents: 64135
diff changeset
   249
        close
64134
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   250
        out_lines.join
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   251
        err_lines.join
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   252
        exit_status.join
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   253
      }
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   254
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   255
      val rc =
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   256
        try { exit_status.join }
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   257
        catch { case Exn.Interrupt() => terminate(); Exn.Interrupt.return_code }
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   258
64136
7c5191489457 close more thoroughly;
wenzelm
parents: 64135
diff changeset
   259
      close
64134
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   260
      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
   261
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   262
      Process_Result(rc, out_lines.join, err_lines.join)
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   263
    }
64131
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
   264
  }
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
   265
f01fca58e0a5 more specific channels;
wenzelm
parents: 64130
diff changeset
   266
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   267
  /* session */
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   268
64166
44925cf6ded1 tuned signature;
wenzelm
parents: 64142
diff changeset
   269
  class Session private[SSH](val options: Options, val session: JSch_Session)
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   270
  {
64166
44925cf6ded1 tuned signature;
wenzelm
parents: 64142
diff changeset
   271
    def update_options(new_options: Options): Session = new Session(new_options, session)
44925cf6ded1 tuned signature;
wenzelm
parents: 64142
diff changeset
   272
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   273
    override def toString: String =
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   274
      (if (session.getUserName == null) "" else session.getUserName + "@") +
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   275
      (if (session.getHost == null) "" else session.getHost) +
64142
954451356017 proper type for Library.using;
wenzelm
parents: 64141
diff changeset
   276
      (if (session.getPort == default_port) "" else ":" + session.getPort) +
64126
42bcd207598d connect session by default;
wenzelm
parents: 64125
diff changeset
   277
      (if (session.isConnected) "" else " (disconnected)")
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   278
64142
954451356017 proper type for Library.using;
wenzelm
parents: 64141
diff changeset
   279
    def close() { session.disconnect }
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   280
64191
wenzelm
parents: 64190
diff changeset
   281
    def sftp(): Sftp =
wenzelm
parents: 64190
diff changeset
   282
    {
wenzelm
parents: 64190
diff changeset
   283
      val kind = "sftp"
wenzelm
parents: 64190
diff changeset
   284
      val channel = session.openChannel(kind).asInstanceOf[ChannelSftp]
wenzelm
parents: 64190
diff changeset
   285
      new Sftp(this, kind, channel)
wenzelm
parents: 64190
diff changeset
   286
    }
64135
865dda40e1cc provide execute operation, similar to Isabelle_System.bash;
wenzelm
parents: 64134
diff changeset
   287
64166
44925cf6ded1 tuned signature;
wenzelm
parents: 64142
diff changeset
   288
    def exec(command: String): Exec =
64129
fce8b7c746b4 support for remote command execution;
wenzelm
parents: 64128
diff changeset
   289
    {
64130
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
   290
      val kind = "exec"
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
   291
      val channel = session.openChannel(kind).asInstanceOf[ChannelExec]
64190
c62b99e3ec07 provide USER_HOME, such that symbolic Path.explode("~") can be used remotely;
wenzelm
parents: 64185
diff changeset
   292
      channel.setCommand("export USER_HOME=\"$HOME\"\n" + command)
64166
44925cf6ded1 tuned signature;
wenzelm
parents: 64142
diff changeset
   293
      new Exec(this, kind, channel)
64129
fce8b7c746b4 support for remote command execution;
wenzelm
parents: 64128
diff changeset
   294
    }
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   295
64191
wenzelm
parents: 64190
diff changeset
   296
    def execute(command: String,
wenzelm
parents: 64190
diff changeset
   297
        progress_stdout: String => Unit = (_: String) => (),
wenzelm
parents: 64190
diff changeset
   298
        progress_stderr: String => Unit = (_: String) => (),
wenzelm
parents: 64190
diff changeset
   299
        strict: Boolean = true): Process_Result =
wenzelm
parents: 64190
diff changeset
   300
      exec(command).result(progress_stdout, progress_stderr, strict)
64137
e9b3d9c1bc5a support for remote tmp dirs;
wenzelm
parents: 64136
diff changeset
   301
e9b3d9c1bc5a support for remote tmp dirs;
wenzelm
parents: 64136
diff changeset
   302
e9b3d9c1bc5a support for remote tmp dirs;
wenzelm
parents: 64136
diff changeset
   303
    /* tmp dirs */
e9b3d9c1bc5a support for remote tmp dirs;
wenzelm
parents: 64136
diff changeset
   304
e9b3d9c1bc5a support for remote tmp dirs;
wenzelm
parents: 64136
diff changeset
   305
    def rm_tree(remote_dir: String): Unit =
e9b3d9c1bc5a support for remote tmp dirs;
wenzelm
parents: 64136
diff changeset
   306
      execute("rm -r -f " + File.bash_string(remote_dir)).check
e9b3d9c1bc5a support for remote tmp dirs;
wenzelm
parents: 64136
diff changeset
   307
e9b3d9c1bc5a support for remote tmp dirs;
wenzelm
parents: 64136
diff changeset
   308
    def tmp_dir(): String =
e9b3d9c1bc5a support for remote tmp dirs;
wenzelm
parents: 64136
diff changeset
   309
      execute("mktemp -d -t tmp.XXXXXXXXXX").check.out
e9b3d9c1bc5a support for remote tmp dirs;
wenzelm
parents: 64136
diff changeset
   310
e9b3d9c1bc5a support for remote tmp dirs;
wenzelm
parents: 64136
diff changeset
   311
    def with_tmp_dir[A](body: String => A): A =
e9b3d9c1bc5a support for remote tmp dirs;
wenzelm
parents: 64136
diff changeset
   312
    {
e9b3d9c1bc5a support for remote tmp dirs;
wenzelm
parents: 64136
diff changeset
   313
      val remote_dir = tmp_dir()
e9b3d9c1bc5a support for remote tmp dirs;
wenzelm
parents: 64136
diff changeset
   314
      try { body(remote_dir) } finally { rm_tree(remote_dir) }
e9b3d9c1bc5a support for remote tmp dirs;
wenzelm
parents: 64136
diff changeset
   315
    }
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   316
  }
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   317
}
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   318
64130
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
   319
class SSH private(val options: Options, val jsch: JSch)
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   320
{
64166
44925cf6ded1 tuned signature;
wenzelm
parents: 64142
diff changeset
   321
  def update_options(new_options: Options): SSH = new SSH(new_options, jsch)
44925cf6ded1 tuned signature;
wenzelm
parents: 64142
diff changeset
   322
64142
954451356017 proper type for Library.using;
wenzelm
parents: 64141
diff changeset
   323
  def open_session(host: String, port: Int = SSH.default_port, user: String = ""): SSH.Session =
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   324
  {
64141
79cd4be708fb support user@host syntax;
wenzelm
parents: 64137
diff changeset
   325
    val session = jsch.getSession(if (user == "") null else user, host, port)
64125
a034dac5ca3c clarified (hardwired!) default (see also jEdit/FTP);
wenzelm
parents: 64124
diff changeset
   326
a034dac5ca3c clarified (hardwired!) default (see also jEdit/FTP);
wenzelm
parents: 64124
diff changeset
   327
    session.setUserInfo(SSH.No_User_Info)
a034dac5ca3c clarified (hardwired!) default (see also jEdit/FTP);
wenzelm
parents: 64124
diff changeset
   328
    session.setConfig("MaxAuthTries", "3")
a034dac5ca3c clarified (hardwired!) default (see also jEdit/FTP);
wenzelm
parents: 64124
diff changeset
   329
64130
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
   330
    if (options.bool("ssh_compression")) {
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   331
      session.setConfig("compression.s2c", "zlib@openssh.com,zlib,none")
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   332
      session.setConfig("compression.c2s", "zlib@openssh.com,zlib,none")
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   333
      session.setConfig("compression_level", "9")
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   334
    }
64125
a034dac5ca3c clarified (hardwired!) default (see also jEdit/FTP);
wenzelm
parents: 64124
diff changeset
   335
64130
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
   336
    session.connect(SSH.connect_timeout(options))
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
   337
    new SSH.Session(options, session)
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   338
  }
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   339
}