# HG changeset patch
# User wenzelm
# Date 1493301415 -7200
# Node ID 6593057089599af92bbb5e6474b683e4736ebe11
# Parent  607f7ad07a60c89eb3fbc6bed0ec111e16462c0a
clarified treatment of default port;

diff -r 607f7ad07a60 -r 659305708959 src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Thu Apr 27 11:41:13 2017 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Thu Apr 27 15:56:55 2017 +0200
@@ -89,7 +89,7 @@
   sealed case class Remote_Build(
     host: String,
     user: String = "",
-    port: Int = SSH.default_port,
+    port: Int = 0,
     shared_home: Boolean = true,
     options: String = "",
     args: String = "")
diff -r 607f7ad07a60 -r 659305708959 src/Pure/Admin/remote_dmg.scala
--- a/src/Pure/Admin/remote_dmg.scala	Thu Apr 27 11:41:13 2017 +0200
+++ b/src/Pure/Admin/remote_dmg.scala	Thu Apr 27 15:56:55 2017 +0200
@@ -32,14 +32,14 @@
     Isabelle_Tool("remote_dmg", "build dmg on remote Mac OS X system", args =>
     {
       Command_Line.tool0 {
-        var port = SSH.default_port
+        var port = 0
         var volume_name = ""
 
         val getopts = Getopts("""
 Usage: isabelle remote_dmg [OPTIONS] USER@HOST TAR_GZ_FILE DMG_FILE
 
   Options are:
-    -p PORT      alternative SSH port (default: """ + SSH.default_port + """)
+    -p PORT      alternative SSH port
     -V NAME      specify volume name
 
   Turn the contents of a tar.gz file into a dmg file -- produced on a remote
diff -r 607f7ad07a60 -r 659305708959 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Thu Apr 27 11:41:13 2017 +0200
+++ b/src/Pure/General/sql.scala	Thu Apr 27 15:56:55 2017 +0200
@@ -325,7 +325,7 @@
     password: String,
     database: String = "",
     host: String = "",
-    port: Int = default_port,
+    port: Int = 0,
     ssh: Option[SSH.Session] = None): Database =
   {
     init_jdbc
@@ -333,7 +333,7 @@
     require(user != "")
 
     val db_host = if (host != "") host else "localhost"
-    val db_port = if (port != default_port) ":" + port else ""
+    val db_port = if (port > 0 && port != default_port) ":" + port else ""
     val db_name = "/" + (if (database != "") database else user)
 
     val (url, name, port_forwarding) =
@@ -344,7 +344,9 @@
           val name = user + "@" + spec
           (url, name, None)
         case Some(ssh) =>
-          val fw = ssh.port_forwarding(remote_host = db_host, remote_port = port)
+          val fw =
+            ssh.port_forwarding(remote_host = db_host,
+              remote_port = if (port > 0) port else default_port)
           val url = "jdbc:postgresql://localhost:" + fw.local_port + db_name
           val name = user + "@" + fw + db_name + " via ssh " + ssh
           (url, name, Some(fw))
diff -r 607f7ad07a60 -r 659305708959 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Thu Apr 27 11:41:13 2017 +0200
+++ b/src/Pure/General/ssh.scala	Thu Apr 27 15:56:55 2017 +0200
@@ -74,9 +74,10 @@
   {
     def update_options(new_options: Options): Context = new Context(new_options, jsch)
 
-    def open_session(host: String, user: String = "", port: Int = default_port): Session =
+    def open_session(host: String, user: String = "", port: Int = 0): Session =
     {
-      val session = jsch.getSession(if (user == "") null else user, host, port)
+      val session =
+        jsch.getSession(if (user == "") null else user, host, if (port > 0) port else default_port)
 
       session.setUserInfo(No_User_Info)
       session.setServerAliveInterval(alive_interval(options))