src/Pure/General/ssh.scala
changeset 65010 a27e9908dcf7
parent 65009 eda9366bbfac
child 65594 659305708959
equal deleted inserted replaced
65009:eda9366bbfac 65010:a27e9908dcf7
   129   }
   129   }
   130 
   130 
   131 
   131 
   132   /* port forwarding */
   132   /* port forwarding */
   133 
   133 
   134   sealed case class Port_Forwarding(ssh: SSH.Session, host: String, port: Int)
   134   object Port_Forwarding
   135   {
   135   {
   136     def close() { ssh.session.delPortForwardingL(host, port) }
   136     def open(ssh: Session,
       
   137       local_host: String, local_port: Int, remote_host: String, remote_port: Int): Port_Forwarding =
       
   138     {
       
   139       val port = ssh.session.setPortForwardingL(local_host, local_port, remote_host, remote_port)
       
   140       new Port_Forwarding(ssh, local_host, port, remote_host, remote_port)
       
   141     }
       
   142   }
       
   143 
       
   144   class Port_Forwarding private[SSH](
       
   145     ssh: SSH.Session,
       
   146     val local_host: String,
       
   147     val local_port: Int,
       
   148     val remote_host: String,
       
   149     val remote_port: Int)
       
   150   {
       
   151     override def toString: String =
       
   152       local_host + ":" + local_port + ":" + remote_host + ":" + remote_port
       
   153 
       
   154     def close() { ssh.session.delPortForwardingL(local_host, local_port) }
   137   }
   155   }
   138 
   156 
   139 
   157 
   140   /* Sftp channel */
   158   /* Sftp channel */
   141 
   159 
   243       user_prefix + host + port_suffix + (if (session.isConnected) "" else " (disconnected)")
   261       user_prefix + host + port_suffix + (if (session.isConnected) "" else " (disconnected)")
   244 
   262 
   245 
   263 
   246     /* port forwarding */
   264     /* port forwarding */
   247 
   265 
   248     def port_forwarding(
   266     def port_forwarding(remote_port: Int, remote_host: String = "localhost",
   249         remote_port: Int, remote_host: String = "localhost",
       
   250         local_port: Int = 0, local_host: String = "localhost"): Port_Forwarding =
   267         local_port: Int = 0, local_host: String = "localhost"): Port_Forwarding =
   251       Port_Forwarding(this, local_host,
   268       Port_Forwarding.open(this, local_host, local_port, remote_host, remote_port)
   252         session.setPortForwardingL(local_host, local_port, remote_host, remote_port))
       
   253 
   269 
   254 
   270 
   255     /* sftp channel */
   271     /* sftp channel */
   256 
   272 
   257     val sftp: ChannelSftp = session.openChannel("sftp").asInstanceOf[ChannelSftp]
   273     val sftp: ChannelSftp = session.openChannel("sftp").asInstanceOf[ChannelSftp]