# HG changeset patch
# User wenzelm
# Date 1476277472 -7200
# Node ID 44925cf6ded185f84adde3fa295c164cc1cbaf81
# Parent  2e1b25d6c1084c053ff25f5104223c136682b9eb
tuned signature;

diff -r 2e1b25d6c108 -r 44925cf6ded1 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Wed Oct 12 11:48:53 2016 +0200
+++ b/src/Pure/General/ssh.scala	Wed Oct 12 15:04:32 2016 +0200
@@ -106,7 +106,7 @@
   /* channel */
 
   class Channel[C <: JSch_Channel] private[SSH](
-    val session: Session, val kind: String, val options: Options, val channel: C)
+    val session: Session, val kind: String, val channel: C)
   {
     override def toString: String = kind + " " + session.toString
 
@@ -118,9 +118,8 @@
 
   private val exec_wait_delay = Time.seconds(0.3)
 
-  class Exec private[SSH](
-    session: Session, kind: String, options: Options, channel: ChannelExec)
-    extends Channel[ChannelExec](session, kind, options, channel)
+  class Exec private[SSH](session: Session, kind: String, channel: ChannelExec)
+    extends Channel[ChannelExec](session, kind, channel)
   {
     def kill(signal: String) { channel.sendSignal(signal) }
 
@@ -134,8 +133,8 @@
     val stdout: InputStream = channel.getInputStream
     val stderr: InputStream = channel.getErrStream
 
-    // after preparing streams
-    channel.connect(connect_timeout(options))
+    // connect after preparing streams
+    channel.connect(connect_timeout(session.options))
 
     def result(
       progress_stdout: String => Unit = (_: String) => (),
@@ -204,11 +203,10 @@
     def is_dir: Boolean = attrs.isDir
   }
 
-  class Sftp private[SSH](
-    session: Session, kind: String, options: Options, channel: ChannelSftp)
-    extends Channel[ChannelSftp](session, kind, options, channel)
+  class Sftp private[SSH](session: Session, kind: String, channel: ChannelSftp)
+    extends Channel[ChannelSftp](session, kind, channel)
   {
-    channel.connect(connect_timeout(options))
+    channel.connect(connect_timeout(session.options))
 
     def home: String = channel.getHome()
 
@@ -268,8 +266,10 @@
 
   /* session */
 
-  class Session private[SSH](val session_options: Options, val session: JSch_Session)
+  class Session private[SSH](val options: Options, val session: JSch_Session)
   {
+    def update_options(new_options: Options): Session = new Session(new_options, session)
+
     override def toString: String =
       (if (session.getUserName == null) "" else session.getUserName + "@") +
       (if (session.getHost == null) "" else session.getHost) +
@@ -279,25 +279,24 @@
     def close() { session.disconnect }
 
     def execute(command: String,
-        options: Options = session_options,
         progress_stdout: String => Unit = (_: String) => (),
         progress_stderr: String => Unit = (_: String) => (),
         strict: Boolean = true): Process_Result =
-      exec(command, options).result(progress_stdout, progress_stderr, strict)
+      exec(command).result(progress_stdout, progress_stderr, strict)
 
-    def exec(command: String, options: Options = session_options): Exec =
+    def exec(command: String): Exec =
     {
       val kind = "exec"
       val channel = session.openChannel(kind).asInstanceOf[ChannelExec]
       channel.setCommand(command)
-      new Exec(this, kind, options, channel)
+      new Exec(this, kind, channel)
     }
 
-    def sftp(options: Options = session_options): Sftp =
+    def sftp(): Sftp =
     {
       val kind = "sftp"
       val channel = session.openChannel(kind).asInstanceOf[ChannelSftp]
-      new Sftp(this, kind, options, channel)
+      new Sftp(this, kind, channel)
     }
 
 
@@ -319,6 +318,8 @@
 
 class SSH private(val options: Options, val jsch: JSch)
 {
+  def update_options(new_options: Options): SSH = new SSH(new_options, jsch)
+
   def open_session(host: String, port: Int = SSH.default_port, user: String = ""): SSH.Session =
   {
     val session = jsch.getSession(if (user == "") null else user, host, port)