support for URL notation;
authorwenzelm
Sat, 22 Oct 2016 19:14:38 +0200
changeset 64347 602483aa7818
parent 64346 5f49765a25ec
child 64348 4c253e84ae62
support for URL notation;
src/Pure/General/mercurial.scala
src/Pure/General/ssh.scala
--- a/src/Pure/General/mercurial.scala	Sat Oct 22 17:27:27 2016 +0200
+++ b/src/Pure/General/mercurial.scala	Sat Oct 22 19:14:38 2016 +0200
@@ -68,6 +68,12 @@
         case Some(ssh) => root_path.expand_env(ssh.settings)
       }
 
+    def root_url: String =
+      ssh match {
+        case None => root.implode
+        case Some(ssh) => ssh.hg_url + root.implode
+      }
+
     override def toString: String =
       ssh match {
         case None => root.implode
--- a/src/Pure/General/ssh.scala	Sat Oct 22 17:27:27 2016 +0200
+++ b/src/Pure/General/ssh.scala	Sat Oct 22 19:14:38 2016 +0200
@@ -226,11 +226,13 @@
   {
     def update_options(new_options: Options): Session = new Session(new_options, session)
 
+    def user_prefix: String = if (session.getUserName == null) "" else session.getUserName + "@"
+    def host: String = if (session.getHost == null) "" else session.getHost
+    def port_suffix: String = if (session.getPort == default_port) "" else ":" + session.getPort
+    def hg_url: String = "ssh://" + user_prefix + host + port_suffix + "/"
+
     override def toString: String =
-      (if (session.getUserName == null) "" else session.getUserName + "@") +
-      (if (session.getHost == null) "" else session.getHost) +
-      (if (session.getPort == default_port) "" else ":" + session.getPort) +
-      (if (session.isConnected) "" else " (disconnected)")
+      user_prefix + host + port_suffix + (if (session.isConnected) "" else " (disconnected)")
 
 
     /* sftp channel */