# HG changeset patch
# User wenzelm
# Date 1493819494 -7200
# Node ID 38139b2067cfecae05cc15d35cee11ffc0a3001b
# Parent  60f4fb867d70625c0c9257d86538ce43579f557e
clarified signature;

diff -r 60f4fb867d70 -r 38139b2067cf src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Wed May 03 15:24:24 2017 +0200
+++ b/src/Pure/Admin/build_log.scala	Wed May 03 15:51:34 2017 +0200
@@ -704,11 +704,11 @@
     val afp_pull_date_table = pull_date_table("afp_pull_date", Prop.afp_version)
 
     def recent(table: SQL.Table, days: Int): String =
-      table.sql_select(table.columns) +
+      table.select(table.columns) +
       " WHERE " + pull_date(table).ident + " > now() - INTERVAL '" + days.max(0) + " days'"
 
     def select_recent(table: SQL.Table, columns: List[SQL.Column], days: Int): String =
-      table.sql_select(columns) +
+      table.select(columns) +
       " INNER JOIN (" + recent(isabelle_pull_date_table, days) + ") AS recent" +
       " ON " + Prop.isabelle_version(table).ident + " = recent." + Prop.isabelle_version.ident
   }
@@ -761,9 +761,9 @@
             List(Data.isabelle_pull_date_table, Data.afp_pull_date_table).foreach(table =>
             {
               db2.create_table(table)
-              using(db2.insert(table))(stmt2 =>
+              db2.using_statement(table.insert())(stmt2 =>
               {
-                using(db.statement(Data.recent(table, days)))(stmt =>
+                db.using_statement(Data.recent(table, days))(stmt =>
                 {
                   val rs = stmt.executeQuery
                   while (rs.next()) {
@@ -780,7 +780,7 @@
     }
 
     def domain(db: SQL.Database, table: SQL.Table, column: SQL.Column): Set[String] =
-      using(db.select(table, List(column), distinct = true))(stmt =>
+      db.using_statement(table.select(List(column), distinct = true))(stmt =>
         SQL.iterator(stmt.executeQuery)(db.string(_, column)).toSet)
 
     def update_meta_info(db: SQL.Database, log_file: Log_File)
@@ -789,8 +789,8 @@
       val table = Data.meta_info_table
 
       db.transaction {
-        using(db.delete(table, Data.log_name.sql_where_equal(log_file.name)))(_.execute)
-        using(db.insert(table))(stmt =>
+        db.using_statement(table.delete(Data.log_name.sql_where_equal(log_file.name)))(_.execute)
+        db.using_statement(table.insert())(stmt =>
         {
           db.set_string(stmt, 1, log_file.name)
           for ((c, i) <- table.columns.tail.zipWithIndex) {
@@ -810,8 +810,8 @@
       val table = Data.sessions_table
 
       db.transaction {
-        using(db.delete(table, Data.log_name.sql_where_equal(log_file.name)))(_.execute)
-        using(db.insert(table))(stmt =>
+        db.using_statement(table.delete(Data.log_name.sql_where_equal(log_file.name)))(_.execute)
+        db.using_statement(table.insert())(stmt =>
         {
           val entries_iterator =
             if (build_info.sessions.isEmpty) Iterator("" -> Session_Entry.empty)
@@ -844,8 +844,8 @@
       val table = Data.ml_statistics_table
 
       db.transaction {
-        using(db.delete(table, Data.log_name.sql_where_equal(log_file.name)))(_.execute)
-        using(db.insert(table))(stmt =>
+        db.using_statement(table.delete(Data.log_name.sql_where_equal(log_file.name)))(_.execute)
+        db.using_statement(table.insert())(stmt =>
         {
           val ml_stats: List[(String, Option[Bytes])] =
             Par_List.map[(String, Session_Entry), (String, Option[Bytes])](
@@ -896,7 +896,7 @@
     {
       val table = Data.meta_info_table
       val columns = table.columns.tail
-      using(db.select(table, columns, Data.log_name.sql_where_equal(log_name)))(stmt =>
+      db.using_statement(table.select(columns, Data.log_name.sql_where_equal(log_name)))(stmt =>
       {
         val rs = stmt.executeQuery
         if (!rs.next) None
@@ -949,7 +949,7 @@
         else (columns1, table1.ident)
 
       val sessions =
-        using(db.statement(SQL.select(columns) + from + " " + where))(stmt =>
+        db.using_statement(SQL.select(columns) + from + " " + where)(stmt =>
         {
           SQL.iterator(stmt.executeQuery)(rs =>
           {
diff -r 60f4fb867d70 -r 38139b2067cf src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Wed May 03 15:24:24 2017 +0200
+++ b/src/Pure/General/sql.scala	Wed May 03 15:51:34 2017 +0200
@@ -141,23 +141,27 @@
       enclosure(columns.map(_.sql_decl(sql_type)) ::: primary_key)
     }
 
-    def sql_create(strict: Boolean, sql_type: Type.Value => String): String =
+    def create(strict: Boolean = false, sql_type: Type.Value => String): String =
       "CREATE TABLE " + (if (strict) "" else "IF NOT EXISTS ") +
         ident + " " + sql_columns(sql_type)
 
-    def sql_create_index(
-        index_name: String, index_columns: List[Column],
-        strict: Boolean, unique: Boolean): String =
+    def create_index(index_name: String, index_columns: List[Column],
+        strict: Boolean = false, unique: Boolean = false): String =
       "CREATE " + (if (unique) "UNIQUE " else "") + "INDEX " +
         (if (strict) "" else "IF NOT EXISTS ") + SQL.ident(index_name) + " ON " +
         ident + " " + enclosure(index_columns.map(_.name))
 
-    def sql_insert: String = "INSERT INTO " + ident + " VALUES " + enclosure(columns.map(_ => "?"))
+    def insert(sql: String = ""): String =
+      "INSERT INTO " + ident + " VALUES " + enclosure(columns.map(_ => "?")) +
+        (if (sql == "") "" else " " + sql)
 
-    def sql_delete: String = "DELETE FROM " + ident
+    def delete(sql: String = ""): String =
+      "DELETE FROM " + ident +
+        (if (sql == "") "" else " " + sql)
 
-    def sql_select(select_columns: List[Column], distinct: Boolean = false): String =
-      select(select_columns, distinct = distinct) + ident
+    def select(select_columns: List[Column], sql: String = "", distinct: Boolean = false): String =
+      SQL.select(select_columns, distinct = distinct) + ident +
+        (if (sql == "") "" else " " + sql)
 
     override def toString: String =
       "TABLE " + ident + " " + sql_columns(sql_type_default)
@@ -208,16 +212,11 @@
 
     /* statements */
 
-    def statement(sql: String): PreparedStatement = connection.prepareStatement(sql)
-
-    def insert(table: Table): PreparedStatement = statement(table.sql_insert)
+    def statement(sql: String): PreparedStatement =
+      connection.prepareStatement(sql)
 
-    def delete(table: Table, sql: String = ""): PreparedStatement =
-      statement(table.sql_delete + (if (sql == "") "" else " " + sql))
-
-    def select(table: Table, columns: List[Column], sql: String = "", distinct: Boolean = false)
-        : PreparedStatement =
-      statement(table.sql_select(columns, distinct = distinct) + (if (sql == "") "" else " " + sql))
+    def using_statement[A](sql: String)(f: PreparedStatement => A): A =
+      using(statement(sql))(f)
 
 
     /* input */
@@ -305,18 +304,18 @@
       iterator(connection.getMetaData.getTables(null, null, "%", null))(_.getString(3)).toList
 
     def create_table(table: Table, strict: Boolean = false, sql: String = ""): Unit =
-      using(statement(table.sql_create(strict, sql_type) + (if (sql == "") "" else " " + sql)))(
-        _.execute())
+      using_statement(
+        table.create(strict, sql_type) + (if (sql == "") "" else " " + sql))(_.execute())
 
     def create_index(table: Table, name: String, columns: List[Column],
         strict: Boolean = false, unique: Boolean = false): Unit =
-      using(statement(table.sql_create_index(name, columns, strict, unique)))(_.execute())
+      using_statement(table.create_index(name, columns, strict, unique))(_.execute())
 
     def create_view(table: Table, strict: Boolean = false): Unit =
     {
       if (strict || !tables.contains(table.name)) {
         val sql = "CREATE VIEW " + table.ident + " AS " + table.expr
-        using(statement(sql))(_.execute())
+        using_statement(sql)(_.execute())
       }
     }
   }
@@ -356,7 +355,7 @@
     def date(rs: ResultSet, column: SQL.Column): Date =
       date_format.parse(string(rs, column))
 
-    def rebuild { using(statement("VACUUM"))(_.execute()) }
+    def rebuild { using_statement("VACUUM")(_.execute()) }
   }
 }
 
diff -r 60f4fb867d70 -r 38139b2067cf src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Wed May 03 15:24:24 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Wed May 03 15:51:34 2017 +0200
@@ -763,7 +763,7 @@
     /* SQL database content */
 
     def read_bytes(db: SQL.Database, name: String, column: SQL.Column): Bytes =
-      using(db.select(Session_Info.table, List(column),
+      db.using_statement(Session_Info.table.select(List(column),
         Session_Info.session_name.sql_where_equal(name)))(stmt =>
       {
         val rs = stmt.executeQuery
@@ -821,9 +821,9 @@
     {
       db.transaction {
         db.create_table(Session_Info.table)
-        using(db.delete(Session_Info.table, Session_Info.session_name.sql_where_equal(name)))(
-          _.execute)
-        using(db.insert(Session_Info.table))(stmt =>
+        db.using_statement(
+          Session_Info.table.delete(Session_Info.session_name.sql_where_equal(name)))(_.execute)
+        db.using_statement(Session_Info.table.insert())(stmt =>
         {
           db.set_string(stmt, 1, name)
           db.set_bytes(stmt, 2, encode_properties(build_log.session_timing))
@@ -864,7 +864,7 @@
     }
 
     def read_build(db: SQL.Database, name: String): Option[Build.Session_Info] =
-      using(db.select(Session_Info.table, Session_Info.build_columns,
+      db.using_statement(Session_Info.table.select(Session_Info.build_columns,
         Session_Info.session_name.sql_where_equal(name)))(stmt =>
       {
         val rs = stmt.executeQuery