src/Pure/General/sql.scala
changeset 78392 27c2fa1db6ed
parent 78391 e47233dbeab7
child 78400 63d55ba90a9f
equal deleted inserted replaced
78391:e47233dbeab7 78392:27c2fa1db6ed
   186       if (body == "") error("Missing SQL body for table " + quote(name))
   186       if (body == "") error("Missing SQL body for table " + quote(name))
   187       else SQL.enclose(body)
   187       else SQL.enclose(body)
   188 
   188 
   189     def query_named: Source = query + " AS " + SQL.ident(name)
   189     def query_named: Source = query + " AS " + SQL.ident(name)
   190 
   190 
   191     def create(strict: Boolean, sql_type: Type.Value => Source): Source = {
   191     def create(sql_type: Type.Value => Source): Source = {
   192       val primary_key =
   192       val primary_key =
   193         columns.filter(_.primary_key).map(_.name) match {
   193         columns.filter(_.primary_key).map(_.name) match {
   194           case Nil => Nil
   194           case Nil => Nil
   195           case keys => List("PRIMARY KEY " + enclosure(keys))
   195           case keys => List("PRIMARY KEY " + enclosure(keys))
   196         }
   196         }
   197       "CREATE TABLE " + (if (strict) "" else "IF NOT EXISTS ") +
   197       "CREATE TABLE " + ident + " " + enclosure(columns.map(_.decl(sql_type)) ::: primary_key)
   198         ident + " " + enclosure(columns.map(_.decl(sql_type)) ::: primary_key)
       
   199     }
   198     }
   200 
   199 
   201     def insert_cmd(cmd: Source = "INSERT", sql: Source = ""): Source =
   200     def insert_cmd(cmd: Source = "INSERT", sql: Source = ""): Source =
   202       cmd + " INTO " + ident + " VALUES " + enclosure(columns.map(_ => "?")) + SQL.separate(sql)
   201       cmd + " INTO " + ident + " VALUES " + enclosure(columns.map(_ => "?")) + SQL.separate(sql)
   203 
   202 
   538       get_tables(pattern = pattern).nonEmpty
   537       get_tables(pattern = pattern).nonEmpty
   539     }
   538     }
   540 
   539 
   541     def exists_table(table: Table): Boolean = exists_table(table.name)
   540     def exists_table(table: Table): Boolean = exists_table(table.name)
   542 
   541 
   543     def create_table(table: Table, strict: Boolean = false, sql: Source = ""): Unit = {
   542     def create_table(table: Table, sql: Source = ""): Unit = {
   544       execute_statement(table.create(strict, sql_type) + SQL.separate(sql))
   543       if (!exists_table(table)) {
   545       if (is_postgresql) {
   544         execute_statement(table.create(sql_type) + SQL.separate(sql))
   546         for (column <- table.columns if column.T == SQL.Type.Bytes) {
   545         if (is_postgresql) {
   547           execute_statement(
   546           for (column <- table.columns if column.T == SQL.Type.Bytes) {
   548             "ALTER TABLE " + table + " ALTER COLUMN " + column + " SET STORAGE EXTERNAL")
   547             execute_statement(
       
   548               "ALTER TABLE " + table + " ALTER COLUMN " + column + " SET STORAGE EXTERNAL")
       
   549           }
   549         }
   550         }
   550       }
   551       }
   551     }
   552     }
   552 
   553 
   553     def create_view(table: Table, strict: Boolean = false): Unit = {
   554     def create_view(table: Table): Unit = {
   554       if (strict || !exists_table(table)) {
   555       if (!exists_table(table)) {
   555         execute_statement("CREATE VIEW " + table + " AS " + { table.query; table.body })
   556         execute_statement("CREATE VIEW " + table + " AS " + { table.query; table.body })
   556       }
   557       }
   557     }
   558     }
   558   }
   559   }
   559 
   560