# HG changeset patch
# User wenzelm
# Date 1476090698 -7200
# Node ID fce8b7c746b4aed5fef6f963b531b5f30a8482a3
# Parent  cc5ea4d648d85c8b223e76970b4e072d2c3eff4c
support for remote command execution;
tuned;

diff -r cc5ea4d648d8 -r fce8b7c746b4 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Mon Oct 10 10:42:14 2016 +0200
+++ b/src/Pure/General/ssh.scala	Mon Oct 10 11:11:38 2016 +0200
@@ -73,6 +73,16 @@
   }
 
 
+  /* remote command execution */
+
+  class Exec private [SSH](val session: Session, val channel: ChannelExec)
+  {
+    override def toString: String = "exec " + session.toString
+
+    def close { channel.disconnect }
+  }
+
+
   /* session */
 
   class Session private[SSH](val session: JSch_Session)
@@ -85,8 +95,14 @@
 
     def close { session.disconnect }
 
-    def channel_exec: ChannelExec =
-      session.openChannel("exec").asInstanceOf[ChannelExec]
+    def exec(command: String, connect_timeout: Time = Time.seconds(60)): Exec =
+    {
+      val channel = session.openChannel("exec").asInstanceOf[ChannelExec]
+      channel.setCommand(command)
+      channel.connect(connect_timeout.ms.toInt)
+
+      new Exec(this, channel)
+    }
 
     def channel_sftp: ChannelSftp =
       session.openChannel("sftp").asInstanceOf[ChannelSftp]
@@ -110,8 +126,7 @@
       session.setConfig("compression_level", "9")
     }
 
-    if (connect_timeout.is_zero) session.connect
-    else session.connect(connect_timeout.ms.toInt)
+    session.connect(connect_timeout.ms.toInt)
 
     new SSH.Session(session)
   }