# HG changeset patch
# User wenzelm
# Date 1489924649 -3600
# Node ID 64da14387b2c7a10789836bf39102cf563061a7b
# Parent  342efc382558b0207f1b9defbecc0319b59536d1
more operations;

diff -r 342efc382558 -r 64da14387b2c src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Sun Mar 19 11:56:56 2017 +0100
+++ b/src/Pure/General/sql.scala	Sun Mar 19 12:57:29 2017 +0100
@@ -136,6 +136,9 @@
     def sql_insert: String =
       "INSERT INTO " + quote_ident(name) + " VALUES " + enclosure(columns.map(_ => "?"))
 
+    def sql_delete: String =
+      "DELETE FROM " + quote_ident(name)
+
     def sql_select(select_columns: List[Column], distinct: Boolean): String =
       "SELECT " + (if (distinct) "DISTINCT " else "") +
       commas(select_columns.map(_.sql_name)) + " FROM " + quote_ident(name)
@@ -193,6 +196,9 @@
 
     def insert_statement(table: Table): PreparedStatement = statement(table.sql_insert)
 
+    def delete_statement(table: Table, sql: String = ""): PreparedStatement =
+      statement(table.sql_delete + (if (sql == "") "" else " " + sql))
+
     def select_statement(table: Table, columns: List[Column],
         sql: String = "", distinct: Boolean = false): PreparedStatement =
       statement(table.sql_select(columns, distinct) + (if (sql == "") "" else " " + sql))