# HG changeset patch
# User wenzelm
# Date 1689422813 -7200
# Node ID 9c2e273d2f0d9bf28f4cb7b58bb9edcc83035096
# Parent  545da61f598987570342457c84a755e0db6c6d1c
clarified signature: more operations;

diff -r 545da61f5989 -r 9c2e273d2f0d src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Sat Jul 15 13:38:01 2023 +0200
+++ b/src/Pure/General/ssh.scala	Sat Jul 15 14:06:53 2023 +0200
@@ -105,7 +105,7 @@
   ) extends System {
     ssh =>
 
-    override def is_local: Boolean = false
+    override def ssh_session: Option[Session] = Some(ssh)
 
     def port_suffix: String = if (port > 0) ":" + port else ""
     def user_prefix: String = if (user.nonEmpty) user + "@" else ""
@@ -357,7 +357,7 @@
       val shutdown_hook =
         Isabelle_System.create_shutdown_hook { cancel() }
 
-      new Server(forward_host, forward_port) {
+      new Server(forward_host, forward_port, ssh) {
         override def toString: String = forward
         override def close(): Unit = {
           cancel()
@@ -368,20 +368,25 @@
     }
   }
 
-  class Server private[SSH](
-    val host: String,
-    val port: Int
-  ) extends AutoCloseable {
-    def defined: Boolean = host.nonEmpty && port > 0
-    override def close(): Unit = ()
-  }
+
+  /* server port forwarding */
 
-  class Local_Server private[SSH](host: String, port: Int) extends Server(host, port) {
-    override def toString: String = if_proper(host, host + ":") + port
-  }
-
-  class No_Server extends Server("", 0) {
-    override def toString: String = "0"
+  def open_server(
+    options: Options,
+    host: String,
+    port: Int = 0,
+    user: String = "",
+    remote_port: Int = 0,
+    remote_host: String = "localhost",
+    local_port: Int = 0,
+    local_host: String = "localhost"
+  ): Server = {
+    val ssh = open_session(options, host, port = port, user = user)
+    try {
+      ssh.open_server(remote_port = remote_port, remote_host = remote_host,
+        local_port = local_port, local_host = local_host, ssh_close = true)
+    }
+    catch { case exn: Throwable => ssh.close(); throw exn }
   }
 
   def local_server(port: Int = 0, host: String = "localhost"): Server =
@@ -389,6 +394,24 @@
 
   val no_server: Server = new No_Server
 
+  class Server private[SSH](
+    val host: String,
+    val port: Int,
+    val system: System
+  ) extends AutoCloseable {
+    def defined: Boolean = host.nonEmpty && port > 0
+    override def close(): Unit = ()
+  }
+
+  class Local_Server private[SSH](host: String, port: Int)
+  extends Server(host, port, Local) {
+    override def toString: String = if_proper(host, host + ":") + port
+  }
+
+  class No_Server extends Server("", 0, Local) {
+    override def toString: String = "0"
+  }
+
 
   /* system operations */
 
@@ -403,7 +426,8 @@
   }
 
   trait System extends AutoCloseable {
-    def is_local: Boolean
+    def ssh_session: Option[Session]
+    def is_local: Boolean = ssh_session.isEmpty
 
     def close(): Unit = ()
 
@@ -463,6 +487,6 @@
   }
 
   object Local extends System {
-    override def is_local: Boolean = true
+    override def ssh_session: Option[Session] = None
   }
 }