# HG changeset patch
# User wenzelm
# Date 1692608030 -7200
# Node ID 3be0437759cf63900daa897ae5f934305d9aab61
# Parent  cfdb586adbbd416b4ecc281c532f5b24e41a16d9
more operations;

diff -r cfdb586adbbd -r 3be0437759cf src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Mon Aug 21 10:53:26 2023 +0200
+++ b/src/Pure/General/sql.scala	Mon Aug 21 10:53:50 2023 +0200
@@ -60,6 +60,10 @@
   val join_inner: Source = " INNER JOIN "
   def join(outer: Boolean): Source = if (outer) join_outer else join_inner
 
+  def MULTI(args: Iterable[Source]): Source =
+    args.iterator.filter(_.nonEmpty).mkString(";\n")
+  def multi(args: Source*): Source = MULTI(args)
+
   def infix(op: Source, args: Iterable[Source]): Source = {
     val body = args.iterator.filter(_.nonEmpty).mkString(" " + op + " ")
     if_proper(body, enclose(body))