equal
deleted
inserted
replaced
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 |