tuned signature;
authorwenzelm
Mon, 11 Mar 2024 20:31:35 +0100
changeset 79859 bc979e334c7d
parent 79858 ee4864e17c11
child 79860 c49cb2a1ec44
tuned signature;
src/Pure/Admin/build_log.scala
src/Pure/General/sql.scala
--- a/src/Pure/Admin/build_log.scala	Mon Mar 11 20:24:59 2024 +0100
+++ b/src/Pure/Admin/build_log.scala	Mon Mar 11 20:31:35 2024 +0100
@@ -1278,7 +1278,7 @@
 
           val columns =
             table1.columns.map(c => c(table1)) :::
-              List(Column.known.copy(expr = Column.log_name(aux_table).defined))
+              List(Column.known.make_expr(Column.log_name(aux_table).defined))
 
           SQL.select(columns, distinct = true) +
             table1.query_named + SQL.join_outer + aux_table.query_named +
--- 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
   }