--- a/src/Pure/Admin/build_log.scala Mon Feb 27 20:30:40 2023 +0100
+++ b/src/Pure/Admin/build_log.scala Mon Feb 27 20:39:08 2023 +0100
@@ -1062,13 +1062,6 @@
val table1 = Data.sessions_table
val table2 = Data.ml_statistics_table
- val where =
- SQL.where(
- SQL.and(
- Data.log_name(table1).equal(log_name),
- Data.session_name(table1).ident + " <> ''",
- if_proper(session_names, Data.session_name(table1).member(session_names))))
-
val columns1 = table1.columns.tail.map(_.apply(table1))
val (columns, from) =
if (ml_statistics) {
@@ -1082,6 +1075,13 @@
}
else (columns1, table1.ident)
+ val where =
+ SQL.where(
+ SQL.and(
+ Data.log_name(table1).equal(log_name),
+ Data.session_name(table1).ident + " <> ''",
+ if_proper(session_names, Data.session_name(table1).member(session_names))))
+
val sessions =
db.using_statement(SQL.select(columns, sql = from + where)) { stmt =>
stmt.execute_query().iterator({ res =>