src/Pure/General/sql.scala
changeset 65280 ef37f5236794
parent 65022 cda3d36aceb2
child 65292 e3bd1e7ddd23
equal deleted inserted replaced
65279:fa62e095d8f1 65280:ef37f5236794
    66 
    66 
    67   /* columns */
    67   /* columns */
    68 
    68 
    69   object Column
    69   object Column
    70   {
    70   {
    71     def bool(name: String, strict: Boolean = true, primary_key: Boolean = false): Column =
    71     def bool(name: String, strict: Boolean = false, primary_key: Boolean = false): Column =
    72       Column(name, Type.Boolean, strict, primary_key)
    72       Column(name, Type.Boolean, strict, primary_key)
    73     def int(name: String, strict: Boolean = true, primary_key: Boolean = false): Column =
    73     def int(name: String, strict: Boolean = false, primary_key: Boolean = false): Column =
    74       Column(name, Type.Int, strict, primary_key)
    74       Column(name, Type.Int, strict, primary_key)
    75     def long(name: String, strict: Boolean = true, primary_key: Boolean = false): Column =
    75     def long(name: String, strict: Boolean = false, primary_key: Boolean = false): Column =
    76       Column(name, Type.Long, strict, primary_key)
    76       Column(name, Type.Long, strict, primary_key)
    77     def double(name: String, strict: Boolean = true, primary_key: Boolean = false): Column =
    77     def double(name: String, strict: Boolean = false, primary_key: Boolean = false): Column =
    78       Column(name, Type.Double, strict, primary_key)
    78       Column(name, Type.Double, strict, primary_key)
    79     def string(name: String, strict: Boolean = true, primary_key: Boolean = false): Column =
    79     def string(name: String, strict: Boolean = false, primary_key: Boolean = false): Column =
    80       Column(name, Type.String, strict, primary_key)
    80       Column(name, Type.String, strict, primary_key)
    81     def bytes(name: String, strict: Boolean = true, primary_key: Boolean = false): Column =
    81     def bytes(name: String, strict: Boolean = false, primary_key: Boolean = false): Column =
    82       Column(name, Type.Bytes, strict, primary_key)
    82       Column(name, Type.Bytes, strict, primary_key)
    83     def date(name: String, strict: Boolean = true, primary_key: Boolean = false): Column =
    83     def date(name: String, strict: Boolean = false, primary_key: Boolean = false): Column =
    84       Column(name, Type.Date, strict, primary_key)
    84       Column(name, Type.Date, strict, primary_key)
    85   }
    85   }
    86 
    86 
    87   sealed case class Column(
    87   sealed case class Column(
    88     name: String, T: Type.Value, strict: Boolean = true, primary_key: Boolean = false)
    88     name: String, T: Type.Value, strict: Boolean = false, primary_key: Boolean = false)
    89   {
    89   {
    90     def sql_name: String = quote_ident(name)
    90     def sql_name: String = quote_ident(name)
    91     def sql_decl(sql_type: Type.Value => String): String =
    91     def sql_decl(sql_type: Type.Value => String): String =
    92       sql_name + " " + sql_type(T) +
    92       sql_name + " " + sql_type(T) +
    93       (if (strict) " NOT NULL" else "") +
    93       (if (strict) " NOT NULL" else "") +
   238     /* tables */
   238     /* tables */
   239 
   239 
   240     def tables: List[String] =
   240     def tables: List[String] =
   241       iterator(connection.getMetaData.getTables(null, null, "%", null))(_.getString(3)).toList
   241       iterator(connection.getMetaData.getTables(null, null, "%", null))(_.getString(3)).toList
   242 
   242 
   243     def create_table(table: Table, strict: Boolean = true, rowid: Boolean = true): Unit =
   243     def create_table(table: Table, strict: Boolean = false, rowid: Boolean = true): Unit =
   244       using(statement(table.sql_create(strict, rowid, sql_type)))(_.execute())
   244       using(statement(table.sql_create(strict, rowid, sql_type)))(_.execute())
   245 
   245 
   246     def drop_table(table: Table, strict: Boolean = true): Unit =
   246     def drop_table(table: Table, strict: Boolean = false): Unit =
   247       using(statement(table.sql_drop(strict)))(_.execute())
   247       using(statement(table.sql_drop(strict)))(_.execute())
   248 
   248 
   249     def create_index(table: Table, name: String, columns: List[Column],
   249     def create_index(table: Table, name: String, columns: List[Column],
   250         strict: Boolean = true, unique: Boolean = false): Unit =
   250         strict: Boolean = false, unique: Boolean = false): Unit =
   251       using(statement(table.sql_create_index(name, columns, strict, unique)))(_.execute())
   251       using(statement(table.sql_create_index(name, columns, strict, unique)))(_.execute())
   252 
   252 
   253     def drop_index(table: Table, name: String, strict: Boolean = true): Unit =
   253     def drop_index(table: Table, name: String, strict: Boolean = false): Unit =
   254       using(statement(table.sql_drop_index(name, strict)))(_.execute())
   254       using(statement(table.sql_drop_index(name, strict)))(_.execute())
   255   }
   255   }
   256 }
   256 }
   257 
   257 
   258 
   258