# HG changeset patch
# User wenzelm
# Date 1678100860 -3600
# Node ID 1bbf29ec9ce33b22c880679647434b0712d18c66
# Parent  7c7f1473e51ad215f3c0ae686283096d6273a178
more operations;

diff -r 7c7f1473e51a -r 1bbf29ec9ce3 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Mon Mar 06 11:39:40 2023 +0100
+++ b/src/Pure/General/sql.scala	Mon Mar 06 12:07:40 2023 +0100
@@ -199,6 +199,10 @@
     def delete(sql: Source = ""): Source =
       "DELETE FROM " + ident + SQL.separate(sql)
 
+    def update(update_columns: List[Column] = Nil, sql: Source = ""): Source =
+      "UPDATE " + ident + " SET " + commas(update_columns.map(c => c.ident + " = ?")) +
+        SQL.separate(sql)
+
     def select(
       select_columns: List[Column] = Nil,
       distinct: Boolean = false,