more operations;
authorwenzelm
Tue, 14 Mar 2023 20:31:08 +0100
changeset 77665 74cd42d053bf
parent 77664 f5d3ade80d15
child 77666 a84f0b1f607d
more operations;
src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Tue Mar 14 20:25:48 2023 +0100
+++ b/src/Pure/General/sql.scala	Tue Mar 14 20:31:08 2023 +0100
@@ -224,6 +224,8 @@
   final class Tables private(val list: List[Table]) extends Iterable[Table] {
     override def toString: String = list.mkString("SQL.Tables(", ", ", ")")
 
+    def ::: (other: Tables): Tables = new Tables(other.list ::: list)
+
     def iterator: Iterator[Table] = list.iterator
 
     // requires transaction