support for SSH in Isabelle/Scala;
authorwenzelm
Sun Oct 09 23:08:40 2016 +0200 (2016-10-09)
changeset 64123a967b5a07f92
parent 64121 f2c8f6b11dcf
child 64124 818265654e60
support for SSH in Isabelle/Scala;
Admin/components/components.sha1
Admin/components/main
src/Pure/General/ssh.scala
src/Pure/build-jars
     1.1 --- a/Admin/components/components.sha1	Sun Oct 09 16:27:01 2016 +0200
     1.2 +++ b/Admin/components/components.sha1	Sun Oct 09 23:08:40 2016 +0200
     1.3 @@ -153,6 +153,7 @@
     1.4  5659440f6b86db29f0c9c0de7249b7e24a647126  scala-2.9.2.tar.gz
     1.5  43b5afbcad575ab6817d2289756ca22fd2ef43a9  spass-3.8ds.tar.gz
     1.6  8d20968603f45a2c640081df1ace6a8b0527452a  sqlite-jdbc-3.8.11.2.tar.gz
     1.7 +2369f06e8d095f9ba26df938b1a96000e535afff  ssh-java-20161009.tar.gz
     1.8  1f4a2053cc1f34fa36c4d9d2ac906ad4ebc863fd  sumatra_pdf-2.1.1.tar.gz
     1.9  601e08d048d8e50b0729429c8928b667d9b6bde9  sumatra_pdf-2.3.2.tar.gz
    1.10  14d46c2eb1a34821703da59d543433f581e91df3  sumatra_pdf-2.4.tar.gz
     2.1 --- a/Admin/components/main	Sun Oct 09 16:27:01 2016 +0200
     2.2 +++ b/Admin/components/main	Sun Oct 09 23:08:40 2016 +0200
     2.3 @@ -12,6 +12,7 @@
     2.4  kodkodi-1.5.2
     2.5  polyml-5.6-1
     2.6  scala-2.11.8
     2.7 +ssh-java-20161009
     2.8  spass-3.8ds
     2.9  sqlite-jdbc-3.8.11.2
    2.10  xz-java-1.5
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/General/ssh.scala	Sun Oct 09 23:08:40 2016 +0200
     3.3 @@ -0,0 +1,107 @@
     3.4 +/*  Title:      Pure/General/ssh.scala
     3.5 +    Author:     Makarius
     3.6 +
     3.7 +Support for Secure Shell.
     3.8 +*/
     3.9 +
    3.10 +package isabelle
    3.11 +
    3.12 +
    3.13 +import com.jcraft.jsch.{JSch, Logger => JSch_Logger, Session => JSch_Session,
    3.14 +  OpenSSHConfig, UserInfo, ChannelExec, ChannelSftp}
    3.15 +
    3.16 +
    3.17 +object SSH
    3.18 +{
    3.19 +  /* init */
    3.20 +
    3.21 +  def apply(config_dir: Path = Path.explode("~/.ssh"),
    3.22 +    config_file: Path = Path.explode("~/.ssh/config"),
    3.23 +    identity_files: List[Path] =
    3.24 +      List("~/.ssh/id_dsa", "~/.ssh/id_ecdsa", "~/.ssh/id_rsa").map(Path.explode(_))): SSH =
    3.25 +  {
    3.26 +    if (!config_dir.is_dir) error("Bad ssh config directory: " + config_dir)
    3.27 +
    3.28 +    val jsch = new JSch
    3.29 +
    3.30 +    if (config_file.is_file)
    3.31 +      jsch.setConfigRepository(OpenSSHConfig.parseFile(File.platform_path(config_file)))
    3.32 +
    3.33 +    val known_hosts = config_dir + Path.explode("known_hosts")
    3.34 +    if (!known_hosts.is_file) known_hosts.file.createNewFile
    3.35 +    jsch.setKnownHosts(File.platform_path(known_hosts))
    3.36 +
    3.37 +    for (identity_file <- identity_files if identity_file.is_file)
    3.38 +      jsch.addIdentity(File.platform_path(identity_file))
    3.39 +
    3.40 +    new SSH(jsch)
    3.41 +  }
    3.42 +
    3.43 +
    3.44 +  /* logging */
    3.45 +
    3.46 +  def logging(verbose: Boolean = true, debug: Boolean = false)
    3.47 +  {
    3.48 +    JSch.setLogger(if (verbose) new Logger(debug) else null)
    3.49 +  }
    3.50 +
    3.51 +  private class Logger(debug: Boolean) extends JSch_Logger
    3.52 +  {
    3.53 +    def isEnabled(level: Int): Boolean = level != JSch_Logger.DEBUG || debug
    3.54 +
    3.55 +    def log(level: Int, msg: String)
    3.56 +    {
    3.57 +      level match {
    3.58 +        case JSch_Logger.ERROR | JSch_Logger.FATAL => Output.error_message(msg)
    3.59 +        case JSch_Logger.WARN => Output.warning(msg)
    3.60 +        case _ => Output.writeln(msg)
    3.61 +      }
    3.62 +    }
    3.63 +  }
    3.64 +
    3.65 +
    3.66 +  /* session */
    3.67 +
    3.68 +  class Session private[SSH](val jsch: JSch, val session: JSch_Session)
    3.69 +  {
    3.70 +    override def toString: String =
    3.71 +      (if (session.getUserName == null) "" else session.getUserName + "@") +
    3.72 +      (if (session.getHost == null) "" else session.getHost) +
    3.73 +      (if (session.getPort == 22) "" else ":" + session.getPort)
    3.74 +
    3.75 +    def open: Session = { session.connect; this }
    3.76 +    def close: Session = { session.disconnect; this }
    3.77 +
    3.78 +    def channel_exec: ChannelExec =
    3.79 +      session.openChannel("exec").asInstanceOf[ChannelExec]
    3.80 +
    3.81 +    def channel_sftp: ChannelSftp =
    3.82 +      session.openChannel("sftp").asInstanceOf[ChannelSftp]
    3.83 +  }
    3.84 +
    3.85 +  object No_User_Info extends UserInfo
    3.86 +  {
    3.87 +    def getPassphrase: String = null
    3.88 +    def getPassword: String = null
    3.89 +    def promptPassword(msg: String): Boolean = false
    3.90 +    def promptPassphrase(msg: String): Boolean = false
    3.91 +    def promptYesNo(msg: String): Boolean = false
    3.92 +    def showMessage(msg: String): Unit = Output.writeln(msg)
    3.93 +  }
    3.94 +}
    3.95 +
    3.96 +class SSH private(val jsch: JSch)
    3.97 +{
    3.98 +  def session(host: String, port: Int = 22, user: String = null,
    3.99 +      compression: Boolean = true): SSH.Session =
   3.100 +  {
   3.101 +    val session = jsch.getSession(user, host, port)
   3.102 +    if (compression) {
   3.103 +      session.setConfig("compression.s2c", "zlib@openssh.com,zlib,none")
   3.104 +      session.setConfig("compression.c2s", "zlib@openssh.com,zlib,none")
   3.105 +      session.setConfig("compression_level", "9")
   3.106 +    }
   3.107 +    session.setUserInfo(SSH.No_User_Info)
   3.108 +    new SSH.Session(jsch, session)
   3.109 +  }
   3.110 +}
     4.1 --- a/src/Pure/build-jars	Sun Oct 09 16:27:01 2016 +0200
     4.2 +++ b/src/Pure/build-jars	Sun Oct 09 23:08:40 2016 +0200
     4.3 @@ -48,6 +48,7 @@
     4.4    General/sha1.scala
     4.5    General/sql.scala
     4.6    General/sqlite.scala
     4.7 +  General/ssh.scala
     4.8    General/symbol.scala
     4.9    General/time.scala
    4.10    General/timing.scala