src/Pure/General/sql.scala
changeset 79859 bc979e334c7d
parent 79858 ee4864e17c11
child 79860 c49cb2a1ec44
--- a/src/Pure/General/sql.scala	Mon Mar 11 20:24:59 2024 +0100
+++ b/src/Pure/General/sql.scala	Mon Mar 11 20:31:35 2024 +0100
@@ -173,7 +173,8 @@
     def where_member_long(set: Iterable[Long]): Source = SQL.where(member_long(set))
     def where_member(set: Iterable[String]): Source = SQL.where(member(set))
 
-    def max: Column = copy(expr = "MAX(" + ident + ")")
+    def make_expr(e: SQL.Source): Column = copy(expr = e)
+    def max: Column = make_expr("MAX(" + ident + ")")
 
     override def toString: Source = ident
   }