clarified signature: discontinue somewhat pointless SSH.Context;

--- a/src/Pure/Admin/isabelle_cronjob.scala	Sun Sep 11 22:29:53 2022 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Sun Sep 11 22:51:54 2022 +0200
@@ -153,8 +153,8 @@
     detect: PostgreSQL.Source = "",
     active: Boolean = true
   ) {
-    def ssh_session(context: SSH.Context): SSH.Session =
-      context.open_session(host = host, user = user, port = port, actual_host = actual_host,
+    def open_session(options: Options): SSH.Session =
+      SSH.open_session(options, host = host, user = user, port = port, actual_host = actual_host,
         proxy_host = proxy_host, proxy_user = proxy_user, proxy_port = proxy_port,
         permissive = proxy_host.nonEmpty)
 
@@ -410,7 +410,7 @@
     val task_name = "build_history-" + r.host
     Logger_Task(task_name,
       { logger =>
-        using(r.ssh_session(logger.ssh_context)) { ssh =>
+        using(r.open_session(logger.options)) { ssh =>
           val results =
             Build_History.remote_build(ssh,
               isabelle_repos,
@@ -443,10 +443,10 @@
 
   object Log_Service {
     def apply(options: Options, progress: Progress = new Progress): Log_Service =
-      new Log_Service(SSH.init_context(options), progress)
+      new Log_Service(options, progress)
   }
 
-  class Log_Service private(val ssh_context: SSH.Context, progress: Progress) {
+  class Log_Service private(val options: Options, progress: Progress) {
     current_log.file.delete
 
     private val thread: Consumer_Thread[String] =
@@ -493,12 +493,11 @@
   }
 
   class Logger private[Isabelle_Cronjob](
-    val log_service: Log_Service,
+    log_service: Log_Service,
     val start_date: Date,
     val task_name: String
   ) {
-    def ssh_context: SSH.Context = log_service.ssh_context
-    def options: Options = ssh_context.options
+    def options: Options = log_service.options
 
     def log(date: Date, msg: String): Unit = log_service.log(date, task_name, msg)
 

--- a/src/Pure/General/ssh.scala	Sun Sep 11 22:29:53 2022 +0200
+++ b/src/Pure/General/ssh.scala	Sun Sep 11 22:51:54 2022 +0200
@@ -58,9 +58,53 @@
     options.int("ssh_alive_count_max")
 
 
-  /* init context */
+  /* open session */
+
+  private def connect_session(
+    options: Options,
+    jsch: JSch,
+    host: String,
+    user: String = "",
+    port: Int = 0,
+    permissive: Boolean = false,
+    nominal_host: String = "",
+    nominal_user: String = "",
+    nominal_port: Option[Int] = None,
+    on_close: () => Unit = () => ()
+  ): Session = {
+    val connect_port = make_port(port)
+    val session = jsch.getSession(proper_string(user).orNull, host, connect_port)
+
+    session.setUserInfo(No_User_Info)
+    session.setServerAliveInterval(alive_interval(options))
+    session.setServerAliveCountMax(alive_count_max(options))
+    session.setConfig("MaxAuthTries", "3")
+    if (permissive) session.setConfig("StrictHostKeyChecking", "no")
+    if (nominal_host != "") session.setHostKeyAlias(nominal_host)
 
-  def init_context(options: Options): Context = {
+    if (options.bool("ssh_compression")) {
+      session.setConfig("compression.s2c", "[e-mail],zlib,none")
+      session.setConfig("compression.c2s", "[e-mail],zlib,none")
+      session.setConfig("compression_level", "9")
+    }
+    session.connect(connect_timeout(options))
+    new Session(options, session, on_close,
+      proper_string(nominal_host) getOrElse host,
+      proper_string(nominal_user) getOrElse user,
+      nominal_port getOrElse connect_port)
+  }
+
+  def open_session(
+    options: Options,
+    host: String,
+    user: String = "",
+    port: Int = 0,
+    actual_host: String = "",
+    proxy_host: String = "",
+    proxy_user: String = "",
+    proxy_port: Int = 0,
+    permissive: Boolean = false
+  ): Session = {
     val config_dir = Path.explode(options.string("ssh_config_dir"))
     if (!config_dir.is_dir) error("Bad ssh config directory: " + config_dir)
 
@@ -84,83 +128,30 @@
       }
     }
 
-    new Context(options, jsch)
-  }
-
-  def open_session(options: Options,
-      host: String, user: String = "", port: Int = 0, actual_host: String = "",
-      proxy_host: String = "", proxy_user: String = "", proxy_port: Int = 0,
-      permissive: Boolean = false): Session =
-    init_context(options).open_session(
-      host = host, user = user, port = port, actual_host = actual_host,
-      proxy_host = proxy_host, proxy_user = proxy_user, proxy_port = proxy_port,
-      permissive = permissive)
+    val connect_host = proper_string(actual_host) getOrElse host
+    val connect_port = make_port(port)
+    if (proxy_host == "") {
+      connect_session(options, jsch, host = connect_host, user = user, port = connect_port)
+    }
+    else {
+      val proxy =
+        connect_session(options, jsch, host = proxy_host, port = proxy_port, user = proxy_user)
 
-  class Context private[SSH](val options: Options, val jsch: JSch) {
-    private def connect_session(
-      host: String,
-      user: String = "",
-      port: Int = 0,
-      permissive: Boolean = false,
-      nominal_host: String = "",
-      nominal_user: String = "",
-      nominal_port: Option[Int] = None,
-      on_close: () => Unit = () => ()
-    ): Session = {
-      val connect_port = make_port(port)
-      val session = jsch.getSession(proper_string(user).orNull, host, connect_port)
+      val fw =
+        try { proxy.port_forwarding(remote_host = connect_host, remote_port = connect_port) }
+        catch { case exn: Throwable => proxy.close(); throw exn }
 
-      session.setUserInfo(No_User_Info)
-      session.setServerAliveInterval(alive_interval(options))
-      session.setServerAliveCountMax(alive_count_max(options))
-      session.setConfig("MaxAuthTries", "3")
-      if (permissive) session.setConfig("StrictHostKeyChecking", "no")
-      if (nominal_host != "") session.setHostKeyAlias(nominal_host)
-
-      if (options.bool("ssh_compression")) {
-        session.setConfig("compression.s2c", "[e-mail],zlib,none")
-        session.setConfig("compression.c2s", "[e-mail],zlib,none")
-        session.setConfig("compression_level", "9")
+      try {
+        connect_session(options, jsch,
+          host = fw.local_host,
+          port = fw.local_port,
+          permissive = permissive,
+          nominal_host = host,
+          nominal_port = Some(connect_port),
+          nominal_user = user, user = user,
+          on_close = { () => fw.close(); proxy.close() })
       }
-      session.connect(connect_timeout(options))
-      new Session(options, session, on_close,
-        proper_string(nominal_host) getOrElse host,
-        proper_string(nominal_user) getOrElse user,
-        nominal_port getOrElse connect_port)
-    }
-
-    def open_session(
-      host: String,
-      user: String = "",
-      port: Int = 0,
-      actual_host: String = "",
-      proxy_host: String = "",
-      proxy_user: String = "",
-      proxy_port: Int = 0,
-      permissive: Boolean = false
-    ): Session = {
-      val connect_host = proper_string(actual_host) getOrElse host
-      val connect_port = make_port(port)
-      if (proxy_host == "") connect_session(host = connect_host, user = user, port = connect_port)
-      else {
-        val proxy = connect_session(host = proxy_host, port = proxy_port, user = proxy_user)
-
-        val fw =
-          try { proxy.port_forwarding(remote_host = connect_host, remote_port = connect_port) }
-          catch { case exn: Throwable => proxy.close(); throw exn }
-
-        try {
-          connect_session(
-            host = fw.local_host,
-            port = fw.local_port,
-            permissive = permissive,
-            nominal_host = host,
-            nominal_port = Some(connect_port),
-            nominal_user = user, user = user,
-            on_close = { () => fw.close(); proxy.close() })
-        }
-        catch { case exn: Throwable => fw.close(); proxy.close(); throw exn }
-      }
+      catch { case exn: Throwable => fw.close(); proxy.close(); throw exn }
     }
   }