# HG changeset patch
# User wenzelm
# Date 1677235539 -3600
# Node ID a10fa21128548283a3b37fefa45b313060a75098
# Parent  6c6797395a3a594dd7cde5eed06b1bdb4ffc4960
clarified signature;

diff -r 6c6797395a3a -r a10fa2112854 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Fri Feb 24 11:38:43 2023 +0100
+++ b/src/Pure/General/sql.scala	Fri Feb 24 11:45:39 2023 +0100
@@ -169,11 +169,11 @@
         (if (strict) "" else "IF NOT EXISTS ") + SQL.ident(index_name) + " ON " +
         ident + " " + enclosure(index_columns.map(_.name))
 
-    def insert_cmd(cmd: Source, sql: Source = ""): Source =
+    def insert_cmd(cmd: Source = "INSERT", sql: Source = ""): Source =
       cmd + " INTO " + ident + " VALUES " + enclosure(columns.map(_ => "?")) +
         (if (sql == "") "" else " " + sql)
 
-    def insert(sql: Source = ""): Source = insert_cmd("INSERT", sql)
+    def insert(sql: Source = ""): Source = insert_cmd(sql = sql)
 
     def delete(sql: Source = ""): Source =
       "DELETE FROM " + ident +
@@ -424,7 +424,7 @@
       date_format.parse(res.string(column))
 
     def insert_permissive(table: SQL.Table, sql: SQL.Source = ""): SQL.Source =
-      table.insert_cmd("INSERT OR IGNORE", sql = sql)
+      table.insert_cmd(cmd = "INSERT OR IGNORE", sql = sql)
   }
 }
 
@@ -500,8 +500,7 @@
     }
 
     def insert_permissive(table: SQL.Table, sql: SQL.Source = ""): SQL.Source =
-      table.insert_cmd("INSERT",
-        sql = sql + (if (sql == "") "" else " ") + "ON CONFLICT DO NOTHING")
+      table.insert_cmd(sql = sql + (if (sql == "") "" else " ") + "ON CONFLICT DO NOTHING")
 
 
     /* notifications: IPC via database server */