# HG changeset patch
# User wenzelm
# Date 1677417331 -3600
# Node ID 7ab9bac1ca96c5b1da16d47050aa7d2000c25f6a
# Parent  324f5821a4a4d597c2f6646d896458a58bed64bf
tuned: prefer typed operations;

diff -r 324f5821a4a4 -r 7ab9bac1ca96 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Sun Feb 26 13:50:07 2023 +0100
+++ b/src/Pure/Admin/build_log.scala	Sun Feb 26 14:15:31 2023 +0100
@@ -719,18 +719,14 @@
       val rev2 = afp_rev.getOrElse("")
       val table = pull_date_table(afp)
 
-      val version1 = Prop.isabelle_version
-      val version2 = Prop.afp_version
-      val eq1 = version1(table).toString + " = " + SQL.string(rev)
-      val eq2 = version2(table).toString + " = " + SQL.string(rev2)
+      val eq_rev = if_proper(rev, Prop.isabelle_version(table).equal(rev))
+      val eq_rev2 = if_proper(rev2, Prop.afp_version(table).equal(rev2))
 
       SQL.Table("recent_pull_date", table.columns,
         table.select(table.columns,
-          "WHERE " + pull_date(afp)(table) + " > " + recent_time(days) +
-          (if (rev != "" && rev2 == "") " OR " + eq1
-           else if (rev == "" && rev2 != "") " OR " + eq2
-           else if (rev != "" && rev2 != "") " OR (" + eq1 + " AND " + eq2 + ")"
-           else "")))
+          SQL.where(
+            SQL.or(pull_date(afp)(table).ident + " > " + recent_time(days),
+              SQL.and(eq_rev, eq_rev2)))))
     }
 
     def select_recent_log_names(days: Int): PostgreSQL.Source = {
@@ -776,9 +772,10 @@
       val a_table =
         SQL.Table("a", a_columns,
           SQL.select(List(log_name, afp_pull_date) ::: table1.columns.tail.map(_.apply(table1))) +
-          table1 + SQL.join_outer + table2 +
-          " ON " + version1(table1) + " = " + version1(table2) +
-          " AND " + version2(table1) + " = " + version2(table2))
+          table1 + SQL.join_outer + table2 + " ON " +
+            SQL.and(
+              version1(table1).ident + " = " + version1(table2).ident,
+              version2(table1).ident + " = " + version2(table2).ident))
 
       val b_columns = log_name :: pull_date() :: a_columns.tail
       val b_table =
@@ -798,9 +795,10 @@
       SQL.Table("isabelle_build_log", c_columns ::: List(ml_statistics),
         {
           SQL.select(c_columns.map(_.apply(c_table)) ::: List(ml_statistics)) +
-          c_table.query_named + SQL.join_outer + ml_statistics_table +
-          " ON " + log_name(c_table) + " = " + log_name(ml_statistics_table) +
-          " AND " + session_name(c_table) + " = " + session_name(ml_statistics_table)
+          c_table.query_named + SQL.join_outer + ml_statistics_table + " ON " +
+            SQL.and(
+              log_name(c_table).ident + " = " + log_name(ml_statistics_table).ident,
+              session_name(c_table).ident + " = " + session_name(ml_statistics_table).ident)
         })
     }
   }
@@ -1063,12 +1061,12 @@
       val table1 = Data.sessions_table
       val table2 = Data.ml_statistics_table
 
-      val where_log_name =
-        Data.log_name(table1).where_equal(log_name) + " AND " +
-        Data.session_name(table1) + " <> ''"
       val where =
-        if (session_names.isEmpty) where_log_name
-        else where_log_name + " AND " + Data.session_name(table1).member(session_names)
+        SQL.where(
+          SQL.and(
+            Data.log_name(table1).where_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) =
@@ -1076,14 +1074,15 @@
           val columns = columns1 ::: List(Data.ml_statistics(table2))
           val join =
             table1.toString + SQL.join_outer + table2 + " ON " +
-            Data.log_name(table1) + " = " + Data.log_name(table2) + " AND " +
-            Data.session_name(table1) + " = " + Data.session_name(table2)
+              SQL.and(
+                Data.log_name(table1).ident + " = " + Data.log_name(table2).ident,
+                Data.session_name(table1).ident + " = " + Data.session_name(table2).ident)
           (columns, SQL.enclose(join))
         }
         else (columns1, table1.ident)
 
       val sessions =
-        db.using_statement(SQL.select(columns) + from + " " + where) { stmt =>
+        db.using_statement(SQL.select(columns) + from + where) { stmt =>
           stmt.execute_query().iterator({ res =>
             val session_name = res.string(Data.session_name)
             val session_entry =