src/Pure/General/sql.scala

--- a/src/Pure/General/sql.scala	Wed May 03 17:00:50 2017 +0200
+++ b/src/Pure/General/sql.scala	Wed May 03 23:04:25 2017 +0200
@@ -150,10 +150,12 @@
         (if (strict) "" else "IF NOT EXISTS ") + SQL.ident(index_name) + " ON " +
         ident + " " + enclosure(index_columns.map(_.name))
 
-    def insert(sql: String = ""): String =
-      "INSERT INTO " + ident + " VALUES " + enclosure(columns.map(_ => "?")) +
+    def insert_cmd(cmd: String, sql: String = ""): String =
+      cmd + " INTO " + ident + " VALUES " + enclosure(columns.map(_ => "?")) +
         (if (sql == "") "" else " " + sql)
 
+    def insert(sql: String = ""): String = insert_cmd("INSERT", sql)
+
     def delete(sql: String = ""): String =
       "DELETE FROM " + ident +
         (if (sql == "") "" else " " + sql)
@@ -216,6 +218,8 @@
     def using_statement[A](sql: String)(f: PreparedStatement => A): A =
       using(statement(sql))(f)
 
+    def insert_permissive(table: Table, sql: String = ""): String
+
 
     /* input */
 
@@ -353,6 +357,9 @@
     def date(rs: ResultSet, column: SQL.Column): Date =
       date_format.parse(string(rs, column))
 
+    def insert_permissive(table: SQL.Table, sql: String = ""): String =
+      table.insert_cmd("INSERT OR IGNORE", sql = sql)
+
     def rebuild { using_statement("VACUUM")(_.execute()) }
   }
 }
@@ -423,6 +430,10 @@
     def date(rs: ResultSet, column: SQL.Column): Date =
       Date.instant(rs.getObject(column.name, classOf[OffsetDateTime]).toInstant)
 
+    def insert_permissive(table: SQL.Table, sql: String = ""): String =
+      table.insert_cmd("INSERT",
+        sql = sql + (if (sql == "") "" else " ") + "ON CONFLICT DO NOTHING")
+
     override def close() { super.close; port_forwarding.foreach(_.close) }
   }
 }