src/Pure/General/ssh.scala

--- a/src/Pure/General/ssh.scala	Thu Oct 13 11:22:27 2016 +0200
+++ b/src/Pure/General/ssh.scala	Thu Oct 13 11:43:40 2016 +0200
@@ -17,9 +17,9 @@
 
 object SSH
 {
-  /* user@host syntax */
+  /* target machine: user@host syntax */
 
-  object User_Host
+  object Target
   {
     val Pattern = "^([^@]+)@(.+)$".r
 
@@ -30,10 +30,10 @@
       }
 
     def unapplySeq(s: String): Option[List[String]] =
-    {
-      val (user, host) = parse(s)
-      Some(List(user, host))
-    }
+      parse(s) match {
+        case (_, "") => None
+        case (user, host) => Some(List(user, host))
+      }
   }
 
   val default_port = 22