src/Pure/General/ssh.scala
changeset 75500 57e292106d71
parent 75480 6c93c13ba3c8
child 75513 36316c6a3fc2
equal deleted inserted replaced
75499:c635368021b6 75500:57e292106d71
    38   }
    38   }
    39 
    39 
    40   val default_port = 22
    40   val default_port = 22
    41   def make_port(port: Int): Int = if (port > 0) port else default_port
    41   def make_port(port: Int): Int = if (port > 0) port else default_port
    42 
    42 
    43   def port_suffix(port: Int, suffix: String = ":"): String =
    43   def port_suffix(port: Int): String =
    44     if (port == default_port) "" else suffix + port
    44     if (port == default_port) "" else ":" + port
    45 
    45 
    46   def user_prefix(user: String): String =
    46   def user_prefix(user: String): String =
    47     proper_string(user) match {
    47     proper_string(user) match {
    48       case None => ""
    48       case None => ""
    49       case Some(name) => name + "@"
    49       case Some(name) => name + "@"
   326     def port: Int = session.getPort
   326     def port: Int = session.getPort
   327 
   327 
   328     override def hg_url: String =
   328     override def hg_url: String =
   329       "ssh://" + user_prefix(nominal_user) + nominal_host + "/"
   329       "ssh://" + user_prefix(nominal_user) + nominal_host + "/"
   330 
   330 
       
   331     override def rsync_prefix: String =
       
   332       user_prefix(nominal_user) + nominal_host + ":"
       
   333 
   331     override def toString: String =
   334     override def toString: String =
   332       user_prefix(session.getUserName) + host + port_suffix(port) +
   335       user_prefix(session.getUserName) + host + port_suffix(port) +
   333       (if (session.isConnected) "" else " (disconnected)")
   336       (if (session.isConnected) "" else " (disconnected)")
   334 
   337 
   335 
   338 
   486 
   489 
   487   trait System extends AutoCloseable {
   490   trait System extends AutoCloseable {
   488     def close(): Unit = ()
   491     def close(): Unit = ()
   489 
   492 
   490     def hg_url: String = ""
   493     def hg_url: String = ""
       
   494 
       
   495     def rsync_prefix: String = ""
       
   496     def rsync_path(path: Path): String = rsync_prefix + expand_path(path)
   491 
   497 
   492     def expand_path(path: Path): Path = path.expand
   498     def expand_path(path: Path): Path = path.expand
   493     def bash_path(path: Path): String = File.bash_path(path)
   499     def bash_path(path: Path): String = File.bash_path(path)
   494     def is_dir(path: Path): Boolean = path.is_dir
   500     def is_dir(path: Path): Boolean = path.is_dir
   495     def is_file(path: Path): Boolean = path.is_file
   501     def is_file(path: Path): Boolean = path.is_file