tuned whitespace in generated SQL;
authorwenzelm
Sun, 26 Feb 2023 14:27:21 +0100
changeset 77377 82fdc7cf9d44
parent 77376 7ab9bac1ca96
child 77378 f047804f4860
tuned whitespace in generated SQL;
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 */