# HG changeset patch
# User wenzelm
# Date 1476174092 -7200
# Node ID 79cd4be708fbd7115f72a27b64a3ce2f9eea2655
# Parent  96d3988711244aa17cb2680f611b0d98e04d9014
support user@host syntax;

diff -r 96d398871124 -r 79cd4be708fb src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Tue Oct 11 09:50:04 2016 +0200
+++ b/src/Pure/General/ssh.scala	Tue Oct 11 10:21:32 2016 +0200
@@ -17,6 +17,26 @@
 
 object SSH
 {
+  /* user@host syntax */
+
+  object User_Host
+  {
+    val Pattern = "^([^@]+)@(.+)$".r
+
+    def parse(s: String): (String, String) =
+      s match {
+        case Pattern(user, host) => (user, host)
+        case _ => ("", s)
+      }
+
+    def unapplySeq(s: String): Option[List[String]] =
+    {
+      val (user, host) = parse(s)
+      Some(List(user, host))
+    }
+  }
+
+
   /* init */
 
   def init(options: Options): SSH =
@@ -297,9 +317,9 @@
 
 class SSH private(val options: Options, val jsch: JSch)
 {
-  def open_session(host: String, port: Int = 22, user: String = null): SSH.Session =
+  def open_session(host: String, port: Int = 22, user: String = ""): SSH.Session =
   {
-    val session = jsch.getSession(user, host, port)
+    val session = jsch.getSession(if (user == "") null else user, host, port)
 
     session.setUserInfo(SSH.No_User_Info)
     session.setConfig("MaxAuthTries", "3")