src/Pure/General/sql.scala
changeset 65698 38139b2067cf
parent 65697 60f4fb867d70
child 65699 9f74d9aa0bdf
equal deleted inserted replaced
65697:60f4fb867d70 65698:38139b2067cf
   139           case keys => List("PRIMARY KEY " + enclosure(keys))
   139           case keys => List("PRIMARY KEY " + enclosure(keys))
   140         }
   140         }
   141       enclosure(columns.map(_.sql_decl(sql_type)) ::: primary_key)
   141       enclosure(columns.map(_.sql_decl(sql_type)) ::: primary_key)
   142     }
   142     }
   143 
   143 
   144     def sql_create(strict: Boolean, sql_type: Type.Value => String): String =
   144     def create(strict: Boolean = false, sql_type: Type.Value => String): String =
   145       "CREATE TABLE " + (if (strict) "" else "IF NOT EXISTS ") +
   145       "CREATE TABLE " + (if (strict) "" else "IF NOT EXISTS ") +
   146         ident + " " + sql_columns(sql_type)
   146         ident + " " + sql_columns(sql_type)
   147 
   147 
   148     def sql_create_index(
   148     def create_index(index_name: String, index_columns: List[Column],
   149         index_name: String, index_columns: List[Column],
   149         strict: Boolean = false, unique: Boolean = false): String =
   150         strict: Boolean, unique: Boolean): String =
       
   151       "CREATE " + (if (unique) "UNIQUE " else "") + "INDEX " +
   150       "CREATE " + (if (unique) "UNIQUE " else "") + "INDEX " +
   152         (if (strict) "" else "IF NOT EXISTS ") + SQL.ident(index_name) + " ON " +
   151         (if (strict) "" else "IF NOT EXISTS ") + SQL.ident(index_name) + " ON " +
   153         ident + " " + enclosure(index_columns.map(_.name))
   152         ident + " " + enclosure(index_columns.map(_.name))
   154 
   153 
   155     def sql_insert: String = "INSERT INTO " + ident + " VALUES " + enclosure(columns.map(_ => "?"))
   154     def insert(sql: String = ""): String =
   156 
   155       "INSERT INTO " + ident + " VALUES " + enclosure(columns.map(_ => "?")) +
   157     def sql_delete: String = "DELETE FROM " + ident
   156         (if (sql == "") "" else " " + sql)
   158 
   157 
   159     def sql_select(select_columns: List[Column], distinct: Boolean = false): String =
   158     def delete(sql: String = ""): String =
   160       select(select_columns, distinct = distinct) + ident
   159       "DELETE FROM " + ident +
       
   160         (if (sql == "") "" else " " + sql)
       
   161 
       
   162     def select(select_columns: List[Column], sql: String = "", distinct: Boolean = false): String =
       
   163       SQL.select(select_columns, distinct = distinct) + ident +
       
   164         (if (sql == "") "" else " " + sql)
   161 
   165 
   162     override def toString: String =
   166     override def toString: String =
   163       "TABLE " + ident + " " + sql_columns(sql_type_default)
   167       "TABLE " + ident + " " + sql_columns(sql_type_default)
   164   }
   168   }
   165 
   169 
   206     }
   210     }
   207 
   211 
   208 
   212 
   209     /* statements */
   213     /* statements */
   210 
   214 
   211     def statement(sql: String): PreparedStatement = connection.prepareStatement(sql)
   215     def statement(sql: String): PreparedStatement =
   212 
   216       connection.prepareStatement(sql)
   213     def insert(table: Table): PreparedStatement = statement(table.sql_insert)
   217 
   214 
   218     def using_statement[A](sql: String)(f: PreparedStatement => A): A =
   215     def delete(table: Table, sql: String = ""): PreparedStatement =
   219       using(statement(sql))(f)
   216       statement(table.sql_delete + (if (sql == "") "" else " " + sql))
       
   217 
       
   218     def select(table: Table, columns: List[Column], sql: String = "", distinct: Boolean = false)
       
   219         : PreparedStatement =
       
   220       statement(table.sql_select(columns, distinct = distinct) + (if (sql == "") "" else " " + sql))
       
   221 
   220 
   222 
   221 
   223     /* input */
   222     /* input */
   224 
   223 
   225     def set_bool(stmt: PreparedStatement, i: Int, x: Boolean) { stmt.setBoolean(i, x) }
   224     def set_bool(stmt: PreparedStatement, i: Int, x: Boolean) { stmt.setBoolean(i, x) }
   303 
   302 
   304     def tables: List[String] =
   303     def tables: List[String] =
   305       iterator(connection.getMetaData.getTables(null, null, "%", null))(_.getString(3)).toList
   304       iterator(connection.getMetaData.getTables(null, null, "%", null))(_.getString(3)).toList
   306 
   305 
   307     def create_table(table: Table, strict: Boolean = false, sql: String = ""): Unit =
   306     def create_table(table: Table, strict: Boolean = false, sql: String = ""): Unit =
   308       using(statement(table.sql_create(strict, sql_type) + (if (sql == "") "" else " " + sql)))(
   307       using_statement(
   309         _.execute())
   308         table.create(strict, sql_type) + (if (sql == "") "" else " " + sql))(_.execute())
   310 
   309 
   311     def create_index(table: Table, name: String, columns: List[Column],
   310     def create_index(table: Table, name: String, columns: List[Column],
   312         strict: Boolean = false, unique: Boolean = false): Unit =
   311         strict: Boolean = false, unique: Boolean = false): Unit =
   313       using(statement(table.sql_create_index(name, columns, strict, unique)))(_.execute())
   312       using_statement(table.create_index(name, columns, strict, unique))(_.execute())
   314 
   313 
   315     def create_view(table: Table, strict: Boolean = false): Unit =
   314     def create_view(table: Table, strict: Boolean = false): Unit =
   316     {
   315     {
   317       if (strict || !tables.contains(table.name)) {
   316       if (strict || !tables.contains(table.name)) {
   318         val sql = "CREATE VIEW " + table.ident + " AS " + table.expr
   317         val sql = "CREATE VIEW " + table.ident + " AS " + table.expr
   319         using(statement(sql))(_.execute())
   318         using_statement(sql)(_.execute())
   320       }
   319       }
   321     }
   320     }
   322   }
   321   }
   323 }
   322 }
   324 
   323 
   354       else set_string(stmt, i, date_format(date))
   353       else set_string(stmt, i, date_format(date))
   355 
   354 
   356     def date(rs: ResultSet, column: SQL.Column): Date =
   355     def date(rs: ResultSet, column: SQL.Column): Date =
   357       date_format.parse(string(rs, column))
   356       date_format.parse(string(rs, column))
   358 
   357 
   359     def rebuild { using(statement("VACUUM"))(_.execute()) }
   358     def rebuild { using_statement("VACUUM")(_.execute()) }
   360   }
   359   }
   361 }
   360 }
   362 
   361 
   363 
   362 
   364 
   363