# HG changeset patch
# User wenzelm
# Date 1489927627 -3600
# Node ID 7f6c738379f42093d8e0f9037b73399be000e6ae
# Parent  b2dc9e3b8ee5b38bd54ee74c7b7726f4162e9f50
more operations;

diff -r b2dc9e3b8ee5 -r 7f6c738379f4 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Sun Mar 19 13:36:19 2017 +0100
+++ b/src/Pure/General/sql.scala	Sun Mar 19 13:47:07 2017 +0100
@@ -234,9 +234,17 @@
     }
     def date(rs: ResultSet, name: String): Date
 
-    def get[A](rs: ResultSet, name: String, f: (ResultSet, String) => A): Option[A] =
+    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] =
     {
-      val x = f(rs, name)
+      val x = f(rs, a)
       if (rs.wasNull) None else Some(x)
     }