more operations;

--- 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,