clarified signature;
authorwenzelm
Wed May 03 15:51:34 2017 +0200 (2017-05-03)
changeset 6569838139b2067cf
parent 65697 60f4fb867d70
child 65699 9f74d9aa0bdf
clarified signature;
src/Pure/Admin/build_log.scala
src/Pure/General/sql.scala
src/Pure/Thy/sessions.scala
     1.1 --- a/src/Pure/Admin/build_log.scala	Wed May 03 15:24:24 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_log.scala	Wed May 03 15:51:34 2017 +0200
     1.3 @@ -704,11 +704,11 @@
     1.4      val afp_pull_date_table = pull_date_table("afp_pull_date", Prop.afp_version)
     1.5  
     1.6      def recent(table: SQL.Table, days: Int): String =
     1.7 -      table.sql_select(table.columns) +
     1.8 +      table.select(table.columns) +
     1.9        " WHERE " + pull_date(table).ident + " > now() - INTERVAL '" + days.max(0) + " days'"
    1.10  
    1.11      def select_recent(table: SQL.Table, columns: List[SQL.Column], days: Int): String =
    1.12 -      table.sql_select(columns) +
    1.13 +      table.select(columns) +
    1.14        " INNER JOIN (" + recent(isabelle_pull_date_table, days) + ") AS recent" +
    1.15        " ON " + Prop.isabelle_version(table).ident + " = recent." + Prop.isabelle_version.ident
    1.16    }
    1.17 @@ -761,9 +761,9 @@
    1.18              List(Data.isabelle_pull_date_table, Data.afp_pull_date_table).foreach(table =>
    1.19              {
    1.20                db2.create_table(table)
    1.21 -              using(db2.insert(table))(stmt2 =>
    1.22 +              db2.using_statement(table.insert())(stmt2 =>
    1.23                {
    1.24 -                using(db.statement(Data.recent(table, days)))(stmt =>
    1.25 +                db.using_statement(Data.recent(table, days))(stmt =>
    1.26                  {
    1.27                    val rs = stmt.executeQuery
    1.28                    while (rs.next()) {
    1.29 @@ -780,7 +780,7 @@
    1.30      }
    1.31  
    1.32      def domain(db: SQL.Database, table: SQL.Table, column: SQL.Column): Set[String] =
    1.33 -      using(db.select(table, List(column), distinct = true))(stmt =>
    1.34 +      db.using_statement(table.select(List(column), distinct = true))(stmt =>
    1.35          SQL.iterator(stmt.executeQuery)(db.string(_, column)).toSet)
    1.36  
    1.37      def update_meta_info(db: SQL.Database, log_file: Log_File)
    1.38 @@ -789,8 +789,8 @@
    1.39        val table = Data.meta_info_table
    1.40  
    1.41        db.transaction {
    1.42 -        using(db.delete(table, Data.log_name.sql_where_equal(log_file.name)))(_.execute)
    1.43 -        using(db.insert(table))(stmt =>
    1.44 +        db.using_statement(table.delete(Data.log_name.sql_where_equal(log_file.name)))(_.execute)
    1.45 +        db.using_statement(table.insert())(stmt =>
    1.46          {
    1.47            db.set_string(stmt, 1, log_file.name)
    1.48            for ((c, i) <- table.columns.tail.zipWithIndex) {
    1.49 @@ -810,8 +810,8 @@
    1.50        val table = Data.sessions_table
    1.51  
    1.52        db.transaction {
    1.53 -        using(db.delete(table, Data.log_name.sql_where_equal(log_file.name)))(_.execute)
    1.54 -        using(db.insert(table))(stmt =>
    1.55 +        db.using_statement(table.delete(Data.log_name.sql_where_equal(log_file.name)))(_.execute)
    1.56 +        db.using_statement(table.insert())(stmt =>
    1.57          {
    1.58            val entries_iterator =
    1.59              if (build_info.sessions.isEmpty) Iterator("" -> Session_Entry.empty)
    1.60 @@ -844,8 +844,8 @@
    1.61        val table = Data.ml_statistics_table
    1.62  
    1.63        db.transaction {
    1.64 -        using(db.delete(table, Data.log_name.sql_where_equal(log_file.name)))(_.execute)
    1.65 -        using(db.insert(table))(stmt =>
    1.66 +        db.using_statement(table.delete(Data.log_name.sql_where_equal(log_file.name)))(_.execute)
    1.67 +        db.using_statement(table.insert())(stmt =>
    1.68          {
    1.69            val ml_stats: List[(String, Option[Bytes])] =
    1.70              Par_List.map[(String, Session_Entry), (String, Option[Bytes])](
    1.71 @@ -896,7 +896,7 @@
    1.72      {
    1.73        val table = Data.meta_info_table
    1.74        val columns = table.columns.tail
    1.75 -      using(db.select(table, columns, Data.log_name.sql_where_equal(log_name)))(stmt =>
    1.76 +      db.using_statement(table.select(columns, Data.log_name.sql_where_equal(log_name)))(stmt =>
    1.77        {
    1.78          val rs = stmt.executeQuery
    1.79          if (!rs.next) None
    1.80 @@ -949,7 +949,7 @@
    1.81          else (columns1, table1.ident)
    1.82  
    1.83        val sessions =
    1.84 -        using(db.statement(SQL.select(columns) + from + " " + where))(stmt =>
    1.85 +        db.using_statement(SQL.select(columns) + from + " " + where)(stmt =>
    1.86          {
    1.87            SQL.iterator(stmt.executeQuery)(rs =>
    1.88            {
     2.1 --- a/src/Pure/General/sql.scala	Wed May 03 15:24:24 2017 +0200
     2.2 +++ b/src/Pure/General/sql.scala	Wed May 03 15:51:34 2017 +0200
     2.3 @@ -141,23 +141,27 @@
     2.4        enclosure(columns.map(_.sql_decl(sql_type)) ::: primary_key)
     2.5      }
     2.6  
     2.7 -    def sql_create(strict: Boolean, sql_type: Type.Value => String): String =
     2.8 +    def create(strict: Boolean = false, sql_type: Type.Value => String): String =
     2.9        "CREATE TABLE " + (if (strict) "" else "IF NOT EXISTS ") +
    2.10          ident + " " + sql_columns(sql_type)
    2.11  
    2.12 -    def sql_create_index(
    2.13 -        index_name: String, index_columns: List[Column],
    2.14 -        strict: Boolean, unique: Boolean): String =
    2.15 +    def create_index(index_name: String, index_columns: List[Column],
    2.16 +        strict: Boolean = false, unique: Boolean = false): String =
    2.17        "CREATE " + (if (unique) "UNIQUE " else "") + "INDEX " +
    2.18          (if (strict) "" else "IF NOT EXISTS ") + SQL.ident(index_name) + " ON " +
    2.19          ident + " " + enclosure(index_columns.map(_.name))
    2.20  
    2.21 -    def sql_insert: String = "INSERT INTO " + ident + " VALUES " + enclosure(columns.map(_ => "?"))
    2.22 +    def insert(sql: String = ""): String =
    2.23 +      "INSERT INTO " + ident + " VALUES " + enclosure(columns.map(_ => "?")) +
    2.24 +        (if (sql == "") "" else " " + sql)
    2.25  
    2.26 -    def sql_delete: String = "DELETE FROM " + ident
    2.27 +    def delete(sql: String = ""): String =
    2.28 +      "DELETE FROM " + ident +
    2.29 +        (if (sql == "") "" else " " + sql)
    2.30  
    2.31 -    def sql_select(select_columns: List[Column], distinct: Boolean = false): String =
    2.32 -      select(select_columns, distinct = distinct) + ident
    2.33 +    def select(select_columns: List[Column], sql: String = "", distinct: Boolean = false): String =
    2.34 +      SQL.select(select_columns, distinct = distinct) + ident +
    2.35 +        (if (sql == "") "" else " " + sql)
    2.36  
    2.37      override def toString: String =
    2.38        "TABLE " + ident + " " + sql_columns(sql_type_default)
    2.39 @@ -208,16 +212,11 @@
    2.40  
    2.41      /* statements */
    2.42  
    2.43 -    def statement(sql: String): PreparedStatement = connection.prepareStatement(sql)
    2.44 -
    2.45 -    def insert(table: Table): PreparedStatement = statement(table.sql_insert)
    2.46 +    def statement(sql: String): PreparedStatement =
    2.47 +      connection.prepareStatement(sql)
    2.48  
    2.49 -    def delete(table: Table, sql: String = ""): PreparedStatement =
    2.50 -      statement(table.sql_delete + (if (sql == "") "" else " " + sql))
    2.51 -
    2.52 -    def select(table: Table, columns: List[Column], sql: String = "", distinct: Boolean = false)
    2.53 -        : PreparedStatement =
    2.54 -      statement(table.sql_select(columns, distinct = distinct) + (if (sql == "") "" else " " + sql))
    2.55 +    def using_statement[A](sql: String)(f: PreparedStatement => A): A =
    2.56 +      using(statement(sql))(f)
    2.57  
    2.58  
    2.59      /* input */
    2.60 @@ -305,18 +304,18 @@
    2.61        iterator(connection.getMetaData.getTables(null, null, "%", null))(_.getString(3)).toList
    2.62  
    2.63      def create_table(table: Table, strict: Boolean = false, sql: String = ""): Unit =
    2.64 -      using(statement(table.sql_create(strict, sql_type) + (if (sql == "") "" else " " + sql)))(
    2.65 -        _.execute())
    2.66 +      using_statement(
    2.67 +        table.create(strict, sql_type) + (if (sql == "") "" else " " + sql))(_.execute())
    2.68  
    2.69      def create_index(table: Table, name: String, columns: List[Column],
    2.70          strict: Boolean = false, unique: Boolean = false): Unit =
    2.71 -      using(statement(table.sql_create_index(name, columns, strict, unique)))(_.execute())
    2.72 +      using_statement(table.create_index(name, columns, strict, unique))(_.execute())
    2.73  
    2.74      def create_view(table: Table, strict: Boolean = false): Unit =
    2.75      {
    2.76        if (strict || !tables.contains(table.name)) {
    2.77          val sql = "CREATE VIEW " + table.ident + " AS " + table.expr
    2.78 -        using(statement(sql))(_.execute())
    2.79 +        using_statement(sql)(_.execute())
    2.80        }
    2.81      }
    2.82    }
    2.83 @@ -356,7 +355,7 @@
    2.84      def date(rs: ResultSet, column: SQL.Column): Date =
    2.85        date_format.parse(string(rs, column))
    2.86  
    2.87 -    def rebuild { using(statement("VACUUM"))(_.execute()) }
    2.88 +    def rebuild { using_statement("VACUUM")(_.execute()) }
    2.89    }
    2.90  }
    2.91  
     3.1 --- a/src/Pure/Thy/sessions.scala	Wed May 03 15:24:24 2017 +0200
     3.2 +++ b/src/Pure/Thy/sessions.scala	Wed May 03 15:51:34 2017 +0200
     3.3 @@ -763,7 +763,7 @@
     3.4      /* SQL database content */
     3.5  
     3.6      def read_bytes(db: SQL.Database, name: String, column: SQL.Column): Bytes =
     3.7 -      using(db.select(Session_Info.table, List(column),
     3.8 +      db.using_statement(Session_Info.table.select(List(column),
     3.9          Session_Info.session_name.sql_where_equal(name)))(stmt =>
    3.10        {
    3.11          val rs = stmt.executeQuery
    3.12 @@ -821,9 +821,9 @@
    3.13      {
    3.14        db.transaction {
    3.15          db.create_table(Session_Info.table)
    3.16 -        using(db.delete(Session_Info.table, Session_Info.session_name.sql_where_equal(name)))(
    3.17 -          _.execute)
    3.18 -        using(db.insert(Session_Info.table))(stmt =>
    3.19 +        db.using_statement(
    3.20 +          Session_Info.table.delete(Session_Info.session_name.sql_where_equal(name)))(_.execute)
    3.21 +        db.using_statement(Session_Info.table.insert())(stmt =>
    3.22          {
    3.23            db.set_string(stmt, 1, name)
    3.24            db.set_bytes(stmt, 2, encode_properties(build_log.session_timing))
    3.25 @@ -864,7 +864,7 @@
    3.26      }
    3.27  
    3.28      def read_build(db: SQL.Database, name: String): Option[Build.Session_Info] =
    3.29 -      using(db.select(Session_Info.table, Session_Info.build_columns,
    3.30 +      db.using_statement(Session_Info.table.select(Session_Info.build_columns,
    3.31          Session_Info.session_name.sql_where_equal(name)))(stmt =>
    3.32        {
    3.33          val rs = stmt.executeQuery