clarified treatment of options;
authorwenzelm
Mon Oct 10 11:48:24 2016 +0200 (2016-10-10)
changeset 64130e17c211a0bb6
parent 64129 fce8b7c746b4
child 64131 f01fca58e0a5
clarified treatment of options;
more uniform channels;
etc/options
src/Pure/General/ssh.scala
     1.1 --- a/etc/options	Mon Oct 10 11:11:38 2016 +0200
     1.2 +++ b/etc/options	Mon Oct 10 11:48:24 2016 +0200
     1.3 @@ -185,3 +185,21 @@
     1.4  
     1.5  public option completion_limit : int = 40
     1.6    -- "limit for completion within the formal context"
     1.7 +
     1.8 +
     1.9 +section "Secure Shell"
    1.10 +
    1.11 +option ssh_config_dir : string = "~/.ssh"
    1.12 +  -- "SSH configuration directory"
    1.13 +
    1.14 +option ssh_config_file : string = "~/.ssh/config"
    1.15 +  -- "main SSH configuration file"
    1.16 +
    1.17 +option ssh_identity_files : string = "~/.ssh/id_dsa:~/.ssh/id_ecdsa:~/.ssh/id_rsa"
    1.18 +  -- "possible SSH identity files (separated by colons)"
    1.19 +
    1.20 +option ssh_compression : bool = true
    1.21 +  -- "enable SSH compression"
    1.22 +
    1.23 +option ssh_connect_timeout : real = 60
    1.24 +  -- "SSH connection timeout (seconds)"
     2.1 --- a/src/Pure/General/ssh.scala	Mon Oct 10 11:11:38 2016 +0200
     2.2 +++ b/src/Pure/General/ssh.scala	Mon Oct 10 11:48:24 2016 +0200
     2.3 @@ -8,22 +8,21 @@
     2.4  
     2.5  
     2.6  import com.jcraft.jsch.{JSch, Logger => JSch_Logger, Session => JSch_Session,
     2.7 -  OpenSSHConfig, UserInfo, ChannelExec, ChannelSftp}
     2.8 +  OpenSSHConfig, UserInfo, Channel => JSch_Channel, ChannelExec, ChannelSftp}
     2.9  
    2.10  
    2.11  object SSH
    2.12  {
    2.13    /* init */
    2.14  
    2.15 -  def init(config_dir: Path = Path.explode("~/.ssh"),
    2.16 -    config_file: Path = Path.explode("~/.ssh/config"),
    2.17 -    identity_files: List[Path] =
    2.18 -      List("~/.ssh/id_dsa", "~/.ssh/id_ecdsa", "~/.ssh/id_rsa").map(Path.explode(_))): SSH =
    2.19 +  def init(options: Options): SSH =
    2.20    {
    2.21 +    val config_dir = Path.explode(options.string("ssh_config_dir"))
    2.22      if (!config_dir.is_dir) error("Bad ssh config directory: " + config_dir)
    2.23  
    2.24      val jsch = new JSch
    2.25  
    2.26 +    val config_file = Path.explode(options.string("ssh_config_file"))
    2.27      if (config_file.is_file)
    2.28        jsch.setConfigRepository(OpenSSHConfig.parseFile(File.platform_path(config_file)))
    2.29  
    2.30 @@ -31,12 +30,17 @@
    2.31      if (!known_hosts.is_file) known_hosts.file.createNewFile
    2.32      jsch.setKnownHosts(File.platform_path(known_hosts))
    2.33  
    2.34 +    val identity_files =
    2.35 +      Library.space_explode(':', options.string("ssh_identity_files")).map(Path.explode(_))
    2.36      for (identity_file <- identity_files if identity_file.is_file)
    2.37        jsch.addIdentity(File.platform_path(identity_file))
    2.38  
    2.39 -    new SSH(jsch)
    2.40 +    new SSH(options, jsch)
    2.41    }
    2.42  
    2.43 +  def connect_timeout(options: Options): Int =
    2.44 +    options.seconds("ssh_connect_timeout").ms.toInt
    2.45 +
    2.46  
    2.47    /* logging */
    2.48  
    2.49 @@ -73,11 +77,12 @@
    2.50    }
    2.51  
    2.52  
    2.53 -  /* remote command execution */
    2.54 +  /* channel: exec, sftp etc. */
    2.55  
    2.56 -  class Exec private [SSH](val session: Session, val channel: ChannelExec)
    2.57 +  class Channel[C <: JSch_Channel] private[SSH](val session: Session,
    2.58 +    val kind: String, val channel_options: Options, val channel: C)
    2.59    {
    2.60 -    override def toString: String = "exec " + session.toString
    2.61 +    override def toString: String = kind + " " + session.toString
    2.62  
    2.63      def close { channel.disconnect }
    2.64    }
    2.65 @@ -85,7 +90,7 @@
    2.66  
    2.67    /* session */
    2.68  
    2.69 -  class Session private[SSH](val session: JSch_Session)
    2.70 +  class Session private[SSH](val session_options: Options, val session: JSch_Session)
    2.71    {
    2.72      override def toString: String =
    2.73        (if (session.getUserName == null) "" else session.getUserName + "@") +
    2.74 @@ -95,39 +100,43 @@
    2.75  
    2.76      def close { session.disconnect }
    2.77  
    2.78 -    def exec(command: String, connect_timeout: Time = Time.seconds(60)): Exec =
    2.79 +    def exec(command: String, options: Options = session_options): Channel[ChannelExec] =
    2.80      {
    2.81 -      val channel = session.openChannel("exec").asInstanceOf[ChannelExec]
    2.82 +      val kind = "exec"
    2.83 +      val channel = session.openChannel(kind).asInstanceOf[ChannelExec]
    2.84        channel.setCommand(command)
    2.85 -      channel.connect(connect_timeout.ms.toInt)
    2.86  
    2.87 -      new Exec(this, channel)
    2.88 +      channel.connect(connect_timeout(options))
    2.89 +      new Channel(this, kind, options, channel)
    2.90      }
    2.91  
    2.92 -    def channel_sftp: ChannelSftp =
    2.93 -      session.openChannel("sftp").asInstanceOf[ChannelSftp]
    2.94 +    def sftp(options: Options = session_options): Channel[ChannelSftp] =
    2.95 +    {
    2.96 +      val kind = "sftp"
    2.97 +      val channel = session.openChannel(kind).asInstanceOf[ChannelSftp]
    2.98 +
    2.99 +      channel.connect(connect_timeout(options))
   2.100 +      new Channel(this, kind, options, channel)
   2.101 +    }
   2.102    }
   2.103  }
   2.104  
   2.105 -class SSH private(val jsch: JSch)
   2.106 +class SSH private(val options: Options, val jsch: JSch)
   2.107  {
   2.108 -  def open_session(host: String, port: Int = 22, user: String = null,
   2.109 -    connect_timeout: Time = Time.seconds(60),
   2.110 -    compression: Boolean = true): SSH.Session =
   2.111 +  def open_session(host: String, port: Int = 22, user: String = null): SSH.Session =
   2.112    {
   2.113      val session = jsch.getSession(user, host, port)
   2.114  
   2.115      session.setUserInfo(SSH.No_User_Info)
   2.116      session.setConfig("MaxAuthTries", "3")
   2.117  
   2.118 -    if (compression) {
   2.119 +    if (options.bool("ssh_compression")) {
   2.120        session.setConfig("compression.s2c", "zlib@openssh.com,zlib,none")
   2.121        session.setConfig("compression.c2s", "zlib@openssh.com,zlib,none")
   2.122        session.setConfig("compression_level", "9")
   2.123      }
   2.124  
   2.125 -    session.connect(connect_timeout.ms.toInt)
   2.126 -
   2.127 -    new SSH.Session(session)
   2.128 +    session.connect(SSH.connect_timeout(options))
   2.129 +    new SSH.Session(options, session)
   2.130    }
   2.131  }