clarified signature;

--- a/src/Pure/General/sql.scala	Fri Jul 14 16:53:39 2023 +0200
+++ b/src/Pure/General/sql.scala	Sat Jul 15 13:38:01 2023 +0200
@@ -575,7 +575,7 @@
 object PostgreSQL {
   type Source = SQL.Source
 
-  val default: SSH.Port_Forwarding = SSH.local_port_forwarding(port = 5432, host = "localhost")
+  val default_server: SSH.Server = SSH.local_server(port = 5432)
 
   lazy val init_jdbc: Unit = Class.forName("org.postgresql.Driver")
 
@@ -594,31 +594,31 @@
 
     if (user == "") error("Undefined database user")
 
-    val db_host = proper_string(host) getOrElse default.host
-    val db_port = if (port > 0) port else default.port
+    val db_host = proper_string(host) getOrElse default_server.host
+    val db_port = if (port > 0) port else default_server.port
     val db_name = proper_string(database) getOrElse user
 
-    val fw =
+    val server =
       ssh match {
         case None =>
-          SSH.local_port_forwarding(port = db_port, host = db_host)
+          SSH.local_server(port = db_port, host = db_host)
         case Some(ssh) =>
-          ssh.port_forwarding(remote_port = db_port, remote_host = db_host, ssh_close = ssh_close)
+          ssh.open_server(remote_port = db_port, remote_host = db_host, ssh_close = ssh_close)
       }
     try {
-      val url = "jdbc:postgresql://" + fw.host + ":" + fw.port + "/" + db_name
-      val name = user + "@" + fw + "/" + db_name + if_proper(ssh, " via ssh " + ssh.get)
+      val url = "jdbc:postgresql://" + server.host + ":" + server.port + "/" + db_name
+      val name = user + "@" + server + "/" + db_name + if_proper(ssh, " via ssh " + ssh.get)
       val connection = DriverManager.getConnection(url, user, password)
       connection.setTransactionIsolation(transaction_isolation)
-      new Database(name, connection, fw)
+      new Database(name, connection, server)
     }
-    catch { case exn: Throwable => fw.close(); throw exn }
+    catch { case exn: Throwable => server.close(); throw exn }
   }
 
   class Database private[PostgreSQL](
     name: String,
     val connection: Connection,
-    val port_forwarding: SSH.Port_Forwarding
+    server: SSH.Server
   ) extends SQL.Database {
     override def toString: String = name
 
@@ -671,6 +671,6 @@
       }
 
 
-    override def close(): Unit = { super.close(); port_forwarding.close() }
+    override def close(): Unit = { super.close(); server.close() }
   }
 }

--- a/src/Pure/General/ssh.scala	Fri Jul 14 16:53:39 2023 +0200
+++ b/src/Pure/General/ssh.scala	Sat Jul 15 13:38:01 2023 +0200
@@ -314,15 +314,15 @@
     }
 
 
-    /* port forwarding */
+    /* open server on remote host */
 
-    def port_forwarding(
+    def open_server(
       remote_port: Int = 0,
       remote_host: String = "localhost",
       local_port: Int = 0,
       local_host: String = "localhost",
       ssh_close: Boolean = false
-    ): Port_Forwarding = {
+    ): Server = {
       val forward_host = local_host
       val forward_port = if (local_port > 0) local_port else Isabelle_System.local_port()
       val forward = List(forward_host, forward_port, remote_host, remote_port).mkString(":")
@@ -335,7 +335,7 @@
         }
         else {
           val result = Synchronized[Exn.Result[Boolean]](Exn.Res(false))
-          val thread = Isabelle_Thread.fork("port_forwarding") {
+          val thread = Isabelle_Thread.fork("ssh_server") {
             val opts =
               forward_option +
                 " " + Config.option("SessionType", "none") +
@@ -357,7 +357,7 @@
       val shutdown_hook =
         Isabelle_System.create_shutdown_hook { cancel() }
 
-      new Port_Forwarding(forward_host, forward_port) {
+      new Server(forward_host, forward_port) {
         override def toString: String = forward
         override def close(): Unit = {
           cancel()
@@ -368,7 +368,7 @@
     }
   }
 
-  class Port_Forwarding private[SSH](
+  class Server private[SSH](
     val host: String,
     val port: Int
   ) extends AutoCloseable {
@@ -376,19 +376,18 @@
     override def close(): Unit = ()
   }
 
-  class Local_Port_Forwarding private[SSH](host: String, port: Int)
-    extends Port_Forwarding(host, port) {
+  class Local_Server private[SSH](host: String, port: Int) extends Server(host, port) {
     override def toString: String = if_proper(host, host + ":") + port
   }
 
-  class No_Port_Forwarding extends Port_Forwarding("", 0) {
+  class No_Server extends Server("", 0) {
     override def toString: String = "0"
   }
 
-  def local_port_forwarding(port: Int = 0, host: String = "localhost"): Port_Forwarding =
-    new Local_Port_Forwarding(host, port)
+  def local_server(port: Int = 0, host: String = "localhost"): Server =
+    new Local_Server(host, port)
 
-  val no_port_forwarding: Port_Forwarding = new No_Port_Forwarding
+  val no_server: Server = new No_Server
 
 
   /* system operations */