diff -r 7ab9bac1ca96 -r 82fdc7cf9d44 src/Pure/General/sql.scala --- a/src/Pure/General/sql.scala Sun Feb 26 14:15:31 2023 +0100 +++ b/src/Pure/General/sql.scala Sun Feb 26 14:27:21 2023 +0100 @@ -77,6 +77,9 @@ def where(sql: Source): Source = if_proper(sql, " WHERE " + sql) + def separate(sql: Source): Source = + (if (sql.isEmpty || sql.startsWith(" ")) "" else " ") + sql + /* types */ @@ -189,17 +192,16 @@ ident + " " + enclosure(index_columns.map(_.name)) def insert_cmd(cmd: Source = "INSERT", sql: Source = ""): Source = - cmd + " INTO " + ident + " VALUES " + enclosure(columns.map(_ => "?")) + - if_proper(sql, " " + sql) + cmd + " INTO " + ident + " VALUES " + enclosure(columns.map(_ => "?")) + SQL.separate(sql) def insert(sql: Source = ""): Source = insert_cmd(sql = sql) def delete(sql: Source = ""): Source = - "DELETE FROM " + ident + if_proper(sql, " " + sql) + "DELETE FROM " + ident + SQL.separate(sql) def select( select_columns: List[Column] = Nil, sql: Source = "", distinct: Boolean = false): Source = - SQL.select(select_columns, distinct = distinct) + ident + if_proper(sql, " " + sql) + SQL.select(select_columns, distinct = distinct) + ident + SQL.separate(sql) override def toString: Source = ident } @@ -383,7 +385,7 @@ } def create_table(table: Table, strict: Boolean = false, sql: Source = ""): Unit = - using_statement(table.create(strict, sql_type) + if_proper(sql, " " + sql))(_.execute()) + using_statement(table.create(strict, sql_type) + SQL.separate(sql))(_.execute()) def create_index(table: Table, name: String, columns: List[Column], strict: Boolean = false, unique: Boolean = false): Unit = @@ -516,7 +518,7 @@ } def insert_permissive(table: SQL.Table, sql: SQL.Source = ""): SQL.Source = - table.insert_cmd(sql = sql + if_proper(sql, " ") + "ON CONFLICT DO NOTHING") + table.insert_cmd(sql = if_proper(sql, sql + " ") + "ON CONFLICT DO NOTHING") /* notifications: IPC via database server */