# HG changeset patch
# User wenzelm
# Date 1493408011 -7200
# Node ID 9b99d61be5af175ed7090ef36997e8df5c07ed19
# Parent  e33b3d57b7cb9f3820441964d155e6471058fd20
tuned signature: less overloading;

diff -r e33b3d57b7cb -r 9b99d61be5af src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Fri Apr 28 20:03:34 2017 +0200
+++ b/src/Pure/General/sql.scala	Fri Apr 28 21:33:31 2017 +0200
@@ -257,33 +257,25 @@
 
     /* output */
 
-    def bool(rs: ResultSet, name: String): Boolean = rs.getBoolean(name)
-    def int(rs: ResultSet, name: String): Int = rs.getInt(name)
-    def long(rs: ResultSet, name: String): Long = rs.getLong(name)
-    def double(rs: ResultSet, name: String): Double = rs.getDouble(name)
-    def string(rs: ResultSet, name: String): String =
+    def bool(rs: ResultSet, column: Column): Boolean = rs.getBoolean(column.name)
+    def int(rs: ResultSet, column: Column): Int = rs.getInt(column.name)
+    def long(rs: ResultSet, column: Column): Long = rs.getLong(column.name)
+    def double(rs: ResultSet, column: Column): Double = rs.getDouble(column.name)
+    def string(rs: ResultSet, column: Column): String =
     {
-      val s = rs.getString(name)
+      val s = rs.getString(column.name)
       if (s == null) "" else s
     }
-    def bytes(rs: ResultSet, name: String): Bytes =
+    def bytes(rs: ResultSet, column: Column): Bytes =
     {
-      val bs = rs.getBytes(name)
+      val bs = rs.getBytes(column.name)
       if (bs == null) Bytes.empty else Bytes(bs)
     }
-    def date(rs: ResultSet, name: String): Date
+    def date(rs: ResultSet, column: Column): Date
 
-    def bool(rs: ResultSet, column: Column): Boolean = bool(rs, column.name)
-    def int(rs: ResultSet, column: Column): Int = int(rs, column.name)
-    def long(rs: ResultSet, column: Column): Long = long(rs, column.name)
-    def double(rs: ResultSet, column: Column): Double = double(rs, column.name)
-    def string(rs: ResultSet, column: Column): String = string(rs, column.name)
-    def bytes(rs: ResultSet, column: Column): Bytes = bytes(rs, column.name)
-    def date(rs: ResultSet, column: Column): Date = date(rs, column.name)
-
-    def get[A, B](rs: ResultSet, a: A, f: (ResultSet, A) => B): Option[B] =
+    def get[A](rs: ResultSet, column: Column, f: (ResultSet, Column) => A): Option[A] =
     {
-      val x = f(rs, a)
+      val x = f(rs, column)
       if (rs.wasNull) None else Some(x)
     }
 
@@ -340,8 +332,8 @@
       if (date == null) set_string(stmt, i, null: String)
       else set_string(stmt, i, date_format(date))
 
-    def date(rs: ResultSet, name: String): Date =
-      date_format.parse(string(rs, name))
+    def date(rs: ResultSet, column: SQL.Column): Date =
+      date_format.parse(string(rs, column))
 
     def rebuild { using(statement("VACUUM"))(_.execute()) }
   }
@@ -408,8 +400,8 @@
       if (date == null) stmt.setObject(i, null)
       else stmt.setObject(i, OffsetDateTime.from(date.to_utc.rep))
 
-    def date(rs: ResultSet, name: String): Date =
-      Date.instant(rs.getObject(name, classOf[OffsetDateTime]).toInstant)
+    def date(rs: ResultSet, column: SQL.Column): Date =
+      Date.instant(rs.getObject(column.name, classOf[OffsetDateTime]).toInstant)
 
     override def close() { super.close; port_forwarding.foreach(_.close) }
   }