src/Pure/General/ssh.scala
author wenzelm
Mon Oct 10 10:25:59 2016 +0200 (2016-10-10)
changeset 64125 a034dac5ca3c
parent 64124 818265654e60
child 64126 42bcd207598d
permissions -rw-r--r--
clarified (hardwired!) default (see also jEdit/FTP);
wenzelm@64123
     1
/*  Title:      Pure/General/ssh.scala
wenzelm@64123
     2
    Author:     Makarius
wenzelm@64123
     3
wenzelm@64124
     4
SSH client based on JSch (see also http://www.jcraft.com/jsch/examples).
wenzelm@64123
     5
*/
wenzelm@64123
     6
wenzelm@64123
     7
package isabelle
wenzelm@64123
     8
wenzelm@64123
     9
wenzelm@64123
    10
import com.jcraft.jsch.{JSch, Logger => JSch_Logger, Session => JSch_Session,
wenzelm@64123
    11
  OpenSSHConfig, UserInfo, ChannelExec, ChannelSftp}
wenzelm@64123
    12
wenzelm@64123
    13
wenzelm@64123
    14
object SSH
wenzelm@64123
    15
{
wenzelm@64123
    16
  /* init */
wenzelm@64123
    17
wenzelm@64123
    18
  def apply(config_dir: Path = Path.explode("~/.ssh"),
wenzelm@64123
    19
    config_file: Path = Path.explode("~/.ssh/config"),
wenzelm@64123
    20
    identity_files: List[Path] =
wenzelm@64123
    21
      List("~/.ssh/id_dsa", "~/.ssh/id_ecdsa", "~/.ssh/id_rsa").map(Path.explode(_))): SSH =
wenzelm@64123
    22
  {
wenzelm@64123
    23
    if (!config_dir.is_dir) error("Bad ssh config directory: " + config_dir)
wenzelm@64123
    24
wenzelm@64123
    25
    val jsch = new JSch
wenzelm@64123
    26
wenzelm@64123
    27
    if (config_file.is_file)
wenzelm@64123
    28
      jsch.setConfigRepository(OpenSSHConfig.parseFile(File.platform_path(config_file)))
wenzelm@64123
    29
wenzelm@64123
    30
    val known_hosts = config_dir + Path.explode("known_hosts")
wenzelm@64123
    31
    if (!known_hosts.is_file) known_hosts.file.createNewFile
wenzelm@64123
    32
    jsch.setKnownHosts(File.platform_path(known_hosts))
wenzelm@64123
    33
wenzelm@64123
    34
    for (identity_file <- identity_files if identity_file.is_file)
wenzelm@64123
    35
      jsch.addIdentity(File.platform_path(identity_file))
wenzelm@64123
    36
wenzelm@64123
    37
    new SSH(jsch)
wenzelm@64123
    38
  }
wenzelm@64123
    39
wenzelm@64123
    40
wenzelm@64123
    41
  /* logging */
wenzelm@64123
    42
wenzelm@64123
    43
  def logging(verbose: Boolean = true, debug: Boolean = false)
wenzelm@64123
    44
  {
wenzelm@64123
    45
    JSch.setLogger(if (verbose) new Logger(debug) else null)
wenzelm@64123
    46
  }
wenzelm@64123
    47
wenzelm@64123
    48
  private class Logger(debug: Boolean) extends JSch_Logger
wenzelm@64123
    49
  {
wenzelm@64123
    50
    def isEnabled(level: Int): Boolean = level != JSch_Logger.DEBUG || debug
wenzelm@64123
    51
wenzelm@64123
    52
    def log(level: Int, msg: String)
wenzelm@64123
    53
    {
wenzelm@64123
    54
      level match {
wenzelm@64123
    55
        case JSch_Logger.ERROR | JSch_Logger.FATAL => Output.error_message(msg)
wenzelm@64123
    56
        case JSch_Logger.WARN => Output.warning(msg)
wenzelm@64123
    57
        case _ => Output.writeln(msg)
wenzelm@64123
    58
      }
wenzelm@64123
    59
    }
wenzelm@64123
    60
  }
wenzelm@64123
    61
wenzelm@64123
    62
wenzelm@64123
    63
  /* session */
wenzelm@64123
    64
wenzelm@64123
    65
  class Session private[SSH](val jsch: JSch, val session: JSch_Session)
wenzelm@64123
    66
  {
wenzelm@64123
    67
    override def toString: String =
wenzelm@64123
    68
      (if (session.getUserName == null) "" else session.getUserName + "@") +
wenzelm@64123
    69
      (if (session.getHost == null) "" else session.getHost) +
wenzelm@64123
    70
      (if (session.getPort == 22) "" else ":" + session.getPort)
wenzelm@64123
    71
wenzelm@64123
    72
    def open: Session = { session.connect; this }
wenzelm@64123
    73
    def close: Session = { session.disconnect; this }
wenzelm@64123
    74
wenzelm@64123
    75
    def channel_exec: ChannelExec =
wenzelm@64123
    76
      session.openChannel("exec").asInstanceOf[ChannelExec]
wenzelm@64123
    77
wenzelm@64123
    78
    def channel_sftp: ChannelSftp =
wenzelm@64123
    79
      session.openChannel("sftp").asInstanceOf[ChannelSftp]
wenzelm@64123
    80
  }
wenzelm@64123
    81
wenzelm@64123
    82
  object No_User_Info extends UserInfo
wenzelm@64123
    83
  {
wenzelm@64123
    84
    def getPassphrase: String = null
wenzelm@64123
    85
    def getPassword: String = null
wenzelm@64123
    86
    def promptPassword(msg: String): Boolean = false
wenzelm@64123
    87
    def promptPassphrase(msg: String): Boolean = false
wenzelm@64123
    88
    def promptYesNo(msg: String): Boolean = false
wenzelm@64123
    89
    def showMessage(msg: String): Unit = Output.writeln(msg)
wenzelm@64123
    90
  }
wenzelm@64123
    91
}
wenzelm@64123
    92
wenzelm@64123
    93
class SSH private(val jsch: JSch)
wenzelm@64123
    94
{
wenzelm@64123
    95
  def session(host: String, port: Int = 22, user: String = null,
wenzelm@64123
    96
      compression: Boolean = true): SSH.Session =
wenzelm@64123
    97
  {
wenzelm@64123
    98
    val session = jsch.getSession(user, host, port)
wenzelm@64125
    99
wenzelm@64125
   100
    session.setUserInfo(SSH.No_User_Info)
wenzelm@64125
   101
    session.setConfig("MaxAuthTries", "3")
wenzelm@64125
   102
wenzelm@64123
   103
    if (compression) {
wenzelm@64123
   104
      session.setConfig("compression.s2c", "zlib@openssh.com,zlib,none")
wenzelm@64123
   105
      session.setConfig("compression.c2s", "zlib@openssh.com,zlib,none")
wenzelm@64123
   106
      session.setConfig("compression_level", "9")
wenzelm@64123
   107
    }
wenzelm@64125
   108
wenzelm@64123
   109
    new SSH.Session(jsch, session)
wenzelm@64123
   110
  }
wenzelm@64123
   111
}