# HG changeset patch
# User wenzelm
# Date 1477156478 -7200
# Node ID 602483aa7818cf532a33ce62170511888c266fc4
# Parent  5f49765a25ec28f9ec399bf6bf300a7434d5e107
support for URL notation;

diff -r 5f49765a25ec -r 602483aa7818 src/Pure/General/mercurial.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
diff -r 5f49765a25ec -r 602483aa7818 src/Pure/General/ssh.scala
--- 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 */