tuned signature;

--- a/src/Pure/Admin/build_log.scala	Wed May 03 15:16:55 2017 +0200
+++ b/src/Pure/Admin/build_log.scala	Wed May 03 15:24:24 2017 +0200
@@ -768,7 +768,7 @@
                   val rs = stmt.executeQuery
                   while (rs.next()) {
                     for ((c, i) <- table.columns.zipWithIndex)
-                      db2.set_string(stmt2, i + 1, db.get(rs, c, db.string _))
+                      db2.set_string(stmt2, i + 1, db.get_string(rs, c))
                     stmt2.execute
                   }
                 })
@@ -904,9 +904,9 @@
           val results =
             columns.map(c => c.name ->
               (if (c.T == SQL.Type.Date)
-                db.get(rs, c, db.date _).map(Log_File.Date_Format(_))
+                db.get_date(rs, c).map(Log_File.Date_Format(_))
                else
-                db.get(rs, c, db.string _)))
+                db.get_string(rs, c)))
           val n = Prop.all_props.length
           val props = for ((x, Some(y)) <- results.take(n)) yield (x, y)
           val settings = for ((x, Some(y)) <- results.drop(n)) yield (x, y)
@@ -958,7 +958,7 @@
               Session_Entry(
                 chapter = db.string(rs, Data.chapter),
                 groups = split_lines(db.string(rs, Data.groups)),
-                threads = db.get(rs, Data.threads, db.int _),
+                threads = db.get_int(rs, Data.threads),
                 timing =
                   Timing(Time.ms(db.long(rs, Data.timing_elapsed)),
                     Time.ms(db.long(rs, Data.timing_cpu)),
@@ -967,10 +967,8 @@
                   Timing(Time.ms(db.long(rs, Data.ml_timing_elapsed)),
                     Time.ms(db.long(rs, Data.ml_timing_cpu)),
                     Time.ms(db.long(rs, Data.ml_timing_gc))),
-                heap_size = db.get(rs, Data.heap_size, db.long _),
-                status =
-                  db.get(rs, Data.status, db.string _).
-                    map(Session_Status.withName(_)),
+                heap_size = db.get_long(rs, Data.heap_size),
+                status = db.get_string(rs, Data.status).map(Session_Status.withName(_)),
                 ml_statistics =
                   if (ml_statistics) uncompress_properties(db.bytes(rs, Data.ml_statistics))
                   else Nil)

--- a/src/Pure/General/sql.scala	Wed May 03 15:16:55 2017 +0200
+++ b/src/Pure/General/sql.scala	Wed May 03 15:24:24 2017 +0200
@@ -290,6 +290,13 @@
       val x = f(rs, column)
       if (rs.wasNull) None else Some(x)
     }
+    def get_bool(rs: ResultSet, column: Column): Option[Boolean] = get(rs, column, bool _)
+    def get_int(rs: ResultSet, column: Column): Option[Int] = get(rs, column, int _)
+    def get_long(rs: ResultSet, column: Column): Option[Long] = get(rs, column, long _)
+    def get_double(rs: ResultSet, column: Column): Option[Double] = get(rs, column, double _)
+    def get_string(rs: ResultSet, column: Column): Option[String] = get(rs, column, string _)
+    def get_bytes(rs: ResultSet, column: Column): Option[Bytes] = get(rs, column, bytes _)
+    def get_date(rs: ResultSet, column: Column): Option[Date] = get(rs, column, date _)
 
 
     /* tables and views */