author | wenzelm |
Thu, 09 Feb 2017 16:58:27 +0100 | |
changeset 65012 | 14641ca387f8 |
parent 65011 | 42bffd1637f0 |
child 65013 | 86308845aa43 |
--- a/src/Pure/General/sql.scala Thu Feb 09 16:56:31 2017 +0100 +++ b/src/Pure/General/sql.scala Thu Feb 09 16:58:27 2017 +0100 @@ -195,6 +195,9 @@ } + + /** SQL database operations **/ + /* results */ def iterator[A](rs: ResultSet)(get: ResultSet => A): Iterator[A] = new Iterator[A] @@ -204,10 +207,6 @@ def next: A = { val x = get(rs); _next = rs.next(); x } } - - - /** SQL database operations **/ - trait Database { /* types */