# HG changeset patch
# User wenzelm
# Date 1476175407 -7200
# Node ID 954451356017976a13d675ab23c38b5809436b83
# Parent  79cd4be708fbd7115f72a27b64a3ce2f9eea2655
proper type for Library.using;
tuned signature;

diff -r 79cd4be708fb -r 954451356017 src/Pure/General/sqlite.scala
--- a/src/Pure/General/sqlite.scala	Tue Oct 11 10:21:32 2016 +0200
+++ b/src/Pure/General/sqlite.scala	Tue Oct 11 10:43:27 2016 +0200
@@ -27,7 +27,7 @@
   {
     override def toString: String = path.toString
 
-    def close { connection.close }
+    def close() { connection.close }
 
     def rebuild { using(statement("VACUUM"))(_.execute()) }
 
diff -r 79cd4be708fb -r 954451356017 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Tue Oct 11 10:21:32 2016 +0200
+++ b/src/Pure/General/ssh.scala	Tue Oct 11 10:43:27 2016 +0200
@@ -36,6 +36,8 @@
     }
   }
 
+  val default_port = 22
+
 
   /* init */
 
@@ -108,7 +110,7 @@
   {
     override def toString: String = kind + " " + session.toString
 
-    def close { channel.disconnect }
+    def close() { channel.disconnect }
   }
 
 
@@ -271,10 +273,10 @@
     override def toString: String =
       (if (session.getUserName == null) "" else session.getUserName + "@") +
       (if (session.getHost == null) "" else session.getHost) +
-      (if (session.getPort == 22) "" else ":" + session.getPort) +
+      (if (session.getPort == default_port) "" else ":" + session.getPort) +
       (if (session.isConnected) "" else " (disconnected)")
 
-    def close { session.disconnect }
+    def close() { session.disconnect }
 
     def execute(command: String,
         options: Options = session_options,
@@ -317,7 +319,7 @@
 
 class SSH private(val options: Options, val jsch: JSch)
 {
-  def open_session(host: String, port: Int = 22, user: String = ""): SSH.Session =
+  def open_session(host: String, port: Int = SSH.default_port, user: String = ""): SSH.Session =
   {
     val session = jsch.getSession(if (user == "") null else user, host, port)