src/Pure/General/ssh.scala
changeset 64126 42bcd207598d
parent 64125 a034dac5ca3c
child 64127 14782d58a503
     1.1 --- a/src/Pure/General/ssh.scala	Mon Oct 10 10:25:59 2016 +0200
     1.2 +++ b/src/Pure/General/ssh.scala	Mon Oct 10 10:33:52 2016 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4  {
     1.5    /* init */
     1.6  
     1.7 -  def apply(config_dir: Path = Path.explode("~/.ssh"),
     1.8 +  def init(config_dir: Path = Path.explode("~/.ssh"),
     1.9      config_file: Path = Path.explode("~/.ssh/config"),
    1.10      identity_files: List[Path] =
    1.11        List("~/.ssh/id_dsa", "~/.ssh/id_ecdsa", "~/.ssh/id_rsa").map(Path.explode(_))): SSH =
    1.12 @@ -62,15 +62,15 @@
    1.13  
    1.14    /* session */
    1.15  
    1.16 -  class Session private[SSH](val jsch: JSch, val session: JSch_Session)
    1.17 +  class Session private[SSH](val session: JSch_Session)
    1.18    {
    1.19      override def toString: String =
    1.20        (if (session.getUserName == null) "" else session.getUserName + "@") +
    1.21        (if (session.getHost == null) "" else session.getHost) +
    1.22 -      (if (session.getPort == 22) "" else ":" + session.getPort)
    1.23 +      (if (session.getPort == 22) "" else ":" + session.getPort) +
    1.24 +      (if (session.isConnected) "" else " (disconnected)")
    1.25  
    1.26 -    def open: Session = { session.connect; this }
    1.27 -    def close: Session = { session.disconnect; this }
    1.28 +    def close { session.disconnect }
    1.29  
    1.30      def channel_exec: ChannelExec =
    1.31        session.openChannel("exec").asInstanceOf[ChannelExec]
    1.32 @@ -92,8 +92,8 @@
    1.33  
    1.34  class SSH private(val jsch: JSch)
    1.35  {
    1.36 -  def session(host: String, port: Int = 22, user: String = null,
    1.37 -      compression: Boolean = true): SSH.Session =
    1.38 +  def open_session(host: String, port: Int = 22, user: String = null,
    1.39 +    compression: Boolean = true): SSH.Session =
    1.40    {
    1.41      val session = jsch.getSession(user, host, port)
    1.42  
    1.43 @@ -106,6 +106,7 @@
    1.44        session.setConfig("compression_level", "9")
    1.45      }
    1.46  
    1.47 -    new SSH.Session(jsch, session)
    1.48 +    session.connect
    1.49 +    new SSH.Session(session)
    1.50    }
    1.51  }