# HG changeset patch
# User wenzelm
# Date 1476088432 -7200
# Node ID 42bcd207598d94b13f2fa1ede8f5bd8e9030cd59
# Parent  a034dac5ca3c8ed69c7a380ba17fb91543b01bc4
connect session by default;
tuned signature;

diff -r a034dac5ca3c -r 42bcd207598d src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Mon Oct 10 10:25:59 2016 +0200
+++ b/src/Pure/General/ssh.scala	Mon Oct 10 10:33:52 2016 +0200
@@ -15,7 +15,7 @@
 {
   /* init */
 
-  def apply(config_dir: Path = Path.explode("~/.ssh"),
+  def init(config_dir: Path = Path.explode("~/.ssh"),
     config_file: Path = Path.explode("~/.ssh/config"),
     identity_files: List[Path] =
       List("~/.ssh/id_dsa", "~/.ssh/id_ecdsa", "~/.ssh/id_rsa").map(Path.explode(_))): SSH =
@@ -62,15 +62,15 @@
 
   /* session */
 
-  class Session private[SSH](val jsch: JSch, val session: JSch_Session)
+  class Session private[SSH](val session: JSch_Session)
   {
     override def toString: String =
       (if (session.getUserName == null) "" else session.getUserName + "@") +
       (if (session.getHost == null) "" else session.getHost) +
-      (if (session.getPort == 22) "" else ":" + session.getPort)
+      (if (session.getPort == 22) "" else ":" + session.getPort) +
+      (if (session.isConnected) "" else " (disconnected)")
 
-    def open: Session = { session.connect; this }
-    def close: Session = { session.disconnect; this }
+    def close { session.disconnect }
 
     def channel_exec: ChannelExec =
       session.openChannel("exec").asInstanceOf[ChannelExec]
@@ -92,8 +92,8 @@
 
 class SSH private(val jsch: JSch)
 {
-  def session(host: String, port: Int = 22, user: String = null,
-      compression: Boolean = true): SSH.Session =
+  def open_session(host: String, port: Int = 22, user: String = null,
+    compression: Boolean = true): SSH.Session =
   {
     val session = jsch.getSession(user, host, port)
 
@@ -106,6 +106,7 @@
       session.setConfig("compression_level", "9")
     }
 
-    new SSH.Session(jsch, session)
+    session.connect
+    new SSH.Session(session)
   }
 }