--- 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
}