--- a/src/Pure/General/sql.scala Wed Feb 22 10:55:38 2023 +0100
+++ b/src/Pure/General/sql.scala Wed Feb 22 21:31:36 2023 +0100
@@ -55,8 +55,12 @@
val join_inner: Source = " INNER JOIN "
def join(outer: Boolean): Source = if (outer) join_outer else join_inner
- def member(x: Source, set: Iterable[String]): Source =
+ def member(x: Source, set: Iterable[String]): Source = {
+ require(set.nonEmpty)
set.iterator.map(a => x + " = " + SQL.string(a)).mkString("(", " OR ", ")")
+ }
+
+ def where_member(x: Source, set: Iterable[String]): Source = " WHERE " + member(x, set)
/* types */