# HG changeset patch
# User wenzelm
# Date 1476633040 -7200
# Node ID 9d51ac055cecb8255488bc7bce0dba49dcff98cf
# Parent  c3197aeae90b31da07b9b26edd6dade4d2adc37c
tuned signature;

diff -r c3197aeae90b -r 9d51ac055cec src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Sun Oct 16 17:44:37 2016 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Sun Oct 16 17:50:40 2016 +0200
@@ -131,7 +131,7 @@
 
   sealed case class Logger_Task(name: String = "", body: Logger => Unit)
 
-  class Log_Service private[Isabelle_Cronjob](progress: Progress, val ssh_context: SSH)
+  class Log_Service private[Isabelle_Cronjob](progress: Progress, val ssh_context: SSH.Context)
   {
     current_log.file.delete
 
@@ -177,7 +177,7 @@
   class Logger private[Isabelle_Cronjob](
     val log_service: Log_Service, val start_date: Date, val task_name: String)
   {
-    def ssh_context: SSH = log_service.ssh_context
+    def ssh_context: SSH.Context = log_service.ssh_context
 
     def log(date: Date, msg: String): Unit = log_service.log(date, task_name, msg)
 
@@ -223,7 +223,7 @@
 
     /* log service */
 
-    val log_service = new Log_Service(progress, SSH.init(Options.init()))
+    val log_service = new Log_Service(progress, SSH.init_context(Options.init()))
 
     def run(start_date: Date, task: Logger_Task) { log_service.run_task(start_date, task) }
 
diff -r c3197aeae90b -r 9d51ac055cec src/Pure/Admin/remote_dmg.scala
--- a/src/Pure/Admin/remote_dmg.scala	Sun Oct 16 17:44:37 2016 +0200
+++ b/src/Pure/Admin/remote_dmg.scala	Sun Oct 16 17:50:40 2016 +0200
@@ -56,7 +56,7 @@
             case _ => getopts.usage()
           }
 
-        val ssh = SSH.init(Options.init)
+        val ssh = SSH.init_context(Options.init)
         using(ssh.open_session(user = user, host = host, port = port))(
           remote_dmg(_, tar_gz_file, dmg_file, volume_name))
       }
diff -r c3197aeae90b -r 9d51ac055cec src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Sun Oct 16 17:44:37 2016 +0200
+++ b/src/Pure/General/ssh.scala	Sun Oct 16 17:50:40 2016 +0200
@@ -38,10 +38,13 @@
 
   val default_port = 22
 
+  def connect_timeout(options: Options): Int =
+    options.seconds("ssh_connect_timeout").ms.toInt
 
-  /* init */
 
-  def init(options: Options): SSH =
+  /* init context */
+
+  def init_context(options: Options): Context =
   {
     val config_dir = Path.explode(options.string("ssh_config_dir"))
     if (!config_dir.is_dir) error("Bad ssh config directory: " + config_dir)
@@ -61,11 +64,30 @@
     for (identity_file <- identity_files if identity_file.is_file)
       jsch.addIdentity(File.platform_path(identity_file))
 
-    new SSH(options, jsch)
+    new Context(options, jsch)
   }
 
-  def connect_timeout(options: Options): Int =
-    options.seconds("ssh_connect_timeout").ms.toInt
+  class Context private[SSH](val options: Options, val jsch: JSch)
+  {
+    def update_options(new_options: Options): Context = new Context(new_options, jsch)
+
+    def open_session(host: String, user: String = "", port: Int = default_port): Session =
+    {
+      val session = jsch.getSession(if (user == "") null else user, host, port)
+
+      session.setUserInfo(No_User_Info)
+      session.setConfig("MaxAuthTries", "3")
+
+      if (options.bool("ssh_compression")) {
+        session.setConfig("compression.s2c", "zlib@openssh.com,zlib,none")
+        session.setConfig("compression.c2s", "zlib@openssh.com,zlib,none")
+        session.setConfig("compression_level", "9")
+      }
+
+      session.connect(connect_timeout(options))
+      new Session(options, session)
+    }
+  }
 
 
   /* logging */
@@ -316,25 +338,3 @@
     }
   }
 }
-
-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, user: String = "", port: Int = SSH.default_port): SSH.Session =
-  {
-    val session = jsch.getSession(if (user == "") null else user, host, port)
-
-    session.setUserInfo(SSH.No_User_Info)
-    session.setConfig("MaxAuthTries", "3")
-
-    if (options.bool("ssh_compression")) {
-      session.setConfig("compression.s2c", "zlib@openssh.com,zlib,none")
-      session.setConfig("compression.c2s", "zlib@openssh.com,zlib,none")
-      session.setConfig("compression_level", "9")
-    }
-
-    session.connect(SSH.connect_timeout(options))
-    new SSH.Session(options, session)
-  }
-}