misc tuning and clarification: more uniform use of optional "sql" in SQL.Table.delete/select;

--- a/src/Pure/Admin/build_log.scala	Sun Feb 26 19:18:24 2023 +0100
+++ b/src/Pure/Admin/build_log.scala	Sun Feb 26 20:19:01 2023 +0100
@@ -723,7 +723,7 @@
       val eq_rev2 = if_proper(rev2, Prop.afp_version(table).equal(rev2))
 
       SQL.Table("recent_pull_date", table.columns,
-        table.select(table.columns,
+        table.select(table.columns, sql =
           SQL.where(
             SQL.or(pull_date(afp)(table).ident + " > " + recent_time(days),
               SQL.and(eq_rev, eq_rev2)))))
@@ -732,8 +732,9 @@
     def select_recent_log_names(days: Int): PostgreSQL.Source = {
       val table1 = meta_info_table
       val table2 = recent_pull_date_table(days)
-      table1.select(List(log_name), distinct = true) + SQL.join_inner + table2.query_named +
-        " ON " + Prop.isabelle_version(table1) + " = " + Prop.isabelle_version(table2)
+      table1.select(List(log_name), distinct = true, sql =
+        SQL.join_inner + table2.query_named +
+        " ON " + Prop.isabelle_version(table1) + " = " + Prop.isabelle_version(table2))
     }
 
     def select_recent_versions(
@@ -1035,7 +1036,7 @@
     def read_meta_info(db: SQL.Database, log_name: String): Option[Meta_Info] = {
       val table = Data.meta_info_table
       val columns = table.columns.tail
-      db.using_statement(table.select(columns, Data.log_name.where_equal(log_name))) { stmt =>
+      db.using_statement(table.select(columns, sql = Data.log_name.where_equal(log_name))) { stmt =>
         val res = stmt.execute_query()
         if (!res.next()) None
         else {

--- a/src/Pure/Admin/build_status.scala	Sun Feb 26 19:18:24 2023 +0100
+++ b/src/Pure/Admin/build_status.scala	Sun Feb 26 20:19:01 2023 +0100
@@ -36,8 +36,8 @@
       columns: List[SQL.Column],
       only_sessions: Set[String]
     ): PostgreSQL.Source = {
-      Build_Log.Data.universal_table.select(columns, distinct = true,
-        sql = "WHERE " +
+      Build_Log.Data.universal_table.select(columns, distinct = true, sql =
+        "WHERE " +
           Build_Log.Data.pull_date(afp) + " > " + Build_Log.Data.recent_time(days(options)) +
           " AND " +
           Build_Log.Data.status.member(

--- a/src/Pure/General/sql.scala	Sun Feb 26 19:18:24 2023 +0100
+++ b/src/Pure/General/sql.scala	Sun Feb 26 20:19:01 2023 +0100
@@ -47,6 +47,9 @@
   def enclose(s: Source): Source = "(" + s + ")"
   def enclosure(ss: Iterable[Source]): Source = ss.mkString("(", ", ", ")")
 
+  def separate(sql: Source): Source =
+    (if (sql.isEmpty || sql.startsWith(" ")) "" else " ") + sql
+
   def select(columns: List[Column] = Nil, distinct: Boolean = false): Source =
     "SELECT " + (if (distinct) "DISTINCT " else "") +
     (if (columns.isEmpty) "*" else commas(columns.map(_.ident))) + " FROM "
@@ -77,9 +80,6 @@
 
   def where(sql: Source): Source = if_proper(sql, " WHERE " + sql)
 
-  def separate(sql: Source): Source =
-    (if (sql.isEmpty || sql.startsWith(" ")) "" else " ") + sql
-
 
   /* types */
 
@@ -200,8 +200,10 @@
       "DELETE FROM " + ident + SQL.separate(sql)
 
     def select(
-        select_columns: List[Column] = Nil, sql: Source = "", distinct: Boolean = false): Source =
-      SQL.select(select_columns, distinct = distinct) + ident + SQL.separate(sql)
+      select_columns: List[Column] = Nil,
+      distinct: Boolean = false,
+      sql: Source = ""
+    ): Source = SQL.select(select_columns, distinct = distinct) + ident + SQL.separate(sql)
 
     override def toString: Source = ident
   }

--- a/src/Pure/Thy/document_build.scala	Sun Feb 26 19:18:24 2023 +0100
+++ b/src/Pure/Thy/document_build.scala	Sun Feb 26 20:19:01 2023 +0100
@@ -70,23 +70,23 @@
           if_proper(name, Data.name.equal(name))))
   }
 
-  def read_documents(db: SQL.Database, session_name: String): List[Document_Input] = {
-    val select = Data.table.select(List(Data.name, Data.sources), Data.where_equal(session_name))
-    db.using_statement(select)(stmt =>
-      stmt.execute_query().iterator({ res =>
-        val name = res.string(Data.name)
-        val sources = res.string(Data.sources)
-        Document_Input(name, SHA1.fake_shasum(sources))
-      }).toList)
-  }
+  def read_documents(db: SQL.Database, session_name: String): List[Document_Input] =
+    db.using_statement(
+      Data.table.select(List(Data.name, Data.sources), sql = Data.where_equal(session_name))
+    ) { stmt =>
+        (stmt.execute_query().iterator { res =>
+          val name = res.string(Data.name)
+          val sources = res.string(Data.sources)
+          Document_Input(name, SHA1.fake_shasum(sources))
+        }).toList
+      }
 
   def read_document(
     db: SQL.Database,
     session_name: String,
     name: String
   ): Option[Document_Output] = {
-    val select = Data.table.select(sql = Data.where_equal(session_name, name))
-    db.using_statement(select)({ stmt =>
+    db.using_statement(Data.table.select(sql = Data.where_equal(session_name, name))) { stmt =>
       val res = stmt.execute_query()
       if (res.next()) {
         val name = res.string(Data.name)
@@ -96,7 +96,7 @@
         Some(Document_Output(name, SHA1.fake_shasum(sources), log_xz, pdf))
       }
       else None
-    })
+    }
   }
 
   def write_document(db: SQL.Database, session_name: String, doc: Document_Output): Unit = {

--- a/src/Pure/Thy/export.scala	Sun Feb 26 19:18:24 2023 +0100
+++ b/src/Pure/Thy/export.scala	Sun Feb 26 20:19:01 2023 +0100
@@ -64,15 +64,15 @@
     }
 
     def readable(db: SQL.Database): Boolean = {
-      val select = Data.table.select(List(Data.name), Data.where_equal(session, theory, name))
-      db.using_statement(select)(stmt => stmt.execute_query().next())
+      db.using_statement(
+        Data.table.select(List(Data.name),
+          sql = Data.where_equal(session, theory, name)))(_.execute_query().next())
     }
 
-    def read(db: SQL.Database, cache: XML.Cache): Option[Entry] = {
-      val select =
+    def read(db: SQL.Database, cache: XML.Cache): Option[Entry] =
+      db.using_statement(
         Data.table.select(List(Data.executable, Data.compressed, Data.body),
-          Data.where_equal(session, theory, name))
-      db.using_statement(select) { stmt =>
+          sql = Data.where_equal(session, theory, name))) { stmt =>
         val res = stmt.execute_query()
         if (res.next()) {
           val executable = res.bool(Data.executable)
@@ -83,27 +83,24 @@
         }
         else None
       }
-    }
-  }
-
-  def read_theory_names(db: SQL.Database, session_name: String): List[String] = {
-    val select =
-      Data.table.select(List(Data.theory_name), Data.where_equal(session_name), distinct = true) +
-      SQL.order_by(List(Data.theory_name))
-    db.using_statement(select)(stmt =>
-      stmt.execute_query().iterator(_.string(Data.theory_name)).toList)
   }
 
-  def read_entry_names(db: SQL.Database, session_name: String): List[Entry_Name] = {
-    val select =
-      Data.table.select(List(Data.theory_name, Data.name), Data.where_equal(session_name)) +
-      SQL.order_by(List(Data.theory_name, Data.name))
-    db.using_statement(select)(stmt =>
-      stmt.execute_query().iterator(res =>
-        Entry_Name(session = session_name,
-          theory = res.string(Data.theory_name),
-          name = res.string(Data.name))).toList)
-  }
+  def read_theory_names(db: SQL.Database, session_name: String): List[String] =
+    db.using_statement(
+      Data.table.select(List(Data.theory_name), distinct = true,
+        sql = Data.where_equal(session_name) + SQL.order_by(List(Data.theory_name)))
+    ) { stmt => stmt.execute_query().iterator(_.string(Data.theory_name)).toList }
+
+  def read_entry_names(db: SQL.Database, session_name: String): List[Entry_Name] =
+    db.using_statement(
+      Data.table.select(List(Data.theory_name, Data.name),
+        sql = Data.where_equal(session_name)) + SQL.order_by(List(Data.theory_name, Data.name))
+    ) { stmt =>
+        stmt.execute_query().iterator(res =>
+          Entry_Name(session = session_name,
+            theory = res.string(Data.theory_name),
+            name = res.string(Data.name))).toList
+      }
 
   def message(msg: String, theory_name: String, name: String): String =
     msg + " " + quote(name) + " for theory " + quote(theory_name)

--- a/src/Pure/Thy/sessions.scala	Sun Feb 26 19:18:24 2023 +0100
+++ b/src/Pure/Thy/sessions.scala	Sun Feb 26 20:19:01 2023 +0100
@@ -1512,8 +1512,9 @@
     /* SQL database content */
 
     def read_bytes(db: SQL.Database, name: String, column: SQL.Column): Bytes =
-      db.using_statement(Session_Info.table.select(List(column),
-        Session_Info.session_name.where_equal(name))) { stmt =>
+      db.using_statement(
+        Session_Info.table.select(List(column),
+          sql = Session_Info.session_name.where_equal(name))) { stmt =>
         val res = stmt.execute_query()
         if (!res.next()) Bytes.empty else res.bytes(column)
       }
@@ -1528,22 +1529,22 @@
       db.transaction {
         db.create_table(Session_Info.table)
         db.using_statement(
-          Session_Info.table.delete(Session_Info.session_name.where_equal(name)))(_.execute())
+          Session_Info.table.delete(sql = Session_Info.session_name.where_equal(name)))(_.execute())
         if (db.isInstanceOf[PostgreSQL.Database]) {
           db.using_statement(Session_Info.augment_table)(_.execute())
         }
 
         db.create_table(Sources.table)
-        db.using_statement(Sources.table.delete(Sources.where_equal(name)))(_.execute())
+        db.using_statement(Sources.table.delete(sql = Sources.where_equal(name)))(_.execute())
 
         db.create_table(Export.Data.table)
         db.using_statement(
-          Export.Data.table.delete(Export.Data.session_name.where_equal(name)))(_.execute())
+          Export.Data.table.delete(sql = Export.Data.session_name.where_equal(name)))(_.execute())
 
         db.create_table(Document_Build.Data.table)
         db.using_statement(
           Document_Build.Data.table.delete(
-            Document_Build.Data.session_name.where_equal(name)))(_.execute())
+            sql = Document_Build.Data.session_name.where_equal(name)))(_.execute())
       }
     }
 
@@ -1557,7 +1558,7 @@
       session_info_exists(db) && {
         db.using_statement(
           Session_Info.table.select(List(Session_Info.session_name),
-            Session_Info.session_name.where_equal(name)))(stmt => stmt.execute_query().next())
+            sql = Session_Info.session_name.where_equal(name)))(_.execute_query().next())
       }
 
     def write_session_info(
@@ -1610,8 +1611,8 @@
 
     def read_build(db: SQL.Database, name: String): Option[Build_Info] = {
       if (db.tables.contains(Session_Info.table.name)) {
-        db.using_statement(Session_Info.table.select(Nil,
-          Session_Info.session_name.where_equal(name))) { stmt =>
+        db.using_statement(
+          Session_Info.table.select(sql = Session_Info.session_name.where_equal(name))) { stmt =>
           val res = stmt.execute_query()
           if (!res.next()) None
           else {
@@ -1652,18 +1653,18 @@
       session_name: String,
       name: String = ""
     ): List[Source_File] = {
-      val select =
-        Sources.table.select(Nil,
+      db.using_statement(
+        Sources.table.select(sql =
           Sources.where_equal(session_name, name = name) + SQL.order_by(List(Sources.name)))
-      db.using_statement(select) { stmt =>
-        (stmt.execute_query().iterator { res =>
-          val res_name = res.string(Sources.name)
-          val digest = SHA1.fake_digest(res.string(Sources.digest))
-          val compressed = res.bool(Sources.compressed)
-          val body = res.bytes(Sources.body)
-          Source_File(res_name, digest, compressed, body, cache.compress)
-        }).toList
-      }
+      ) { stmt =>
+          (stmt.execute_query().iterator { res =>
+            val res_name = res.string(Sources.name)
+            val digest = SHA1.fake_digest(res.string(Sources.digest))
+            val compressed = res.bool(Sources.compressed)
+            val body = res.bytes(Sources.body)
+            Source_File(res_name, digest, compressed, body, cache.compress)
+          }).toList
+        }
     }
   }
 }

--- a/src/Pure/Tools/build_process.scala	Sun Feb 26 19:18:24 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Sun Feb 26 20:19:01 2023 +0100
@@ -302,7 +302,7 @@
     }
 
     def read_pending(db: SQL.Database): List[Entry] =
-      db.using_statement(Pending.table.select() + SQL.order_by(List(Pending.name))) { stmt =>
+      db.using_statement(Pending.table.select(sql = SQL.order_by(List(Pending.name)))) { stmt =>
         List.from(
           stmt.execute_query().iterator { res =>
             val name = res.string(Pending.name)
@@ -318,8 +318,8 @@
 
       if (delete.nonEmpty) {
         db.using_statement(
-          Pending.table.delete() + SQL.where(Generic.sql_member(names = delete.map(_.name)))
-        )(_.execute())
+          Pending.table.delete(
+            sql = SQL.where(Generic.sql_member(names = delete.map(_.name)))))(_.execute())
       }
 
       for (entry <- insert) {
@@ -335,7 +335,7 @@
     }
 
     def read_running(db: SQL.Database): List[Build_Job.Abstract] =
-      db.using_statement(Running.table.select() + SQL.order_by(List(Running.name))) { stmt =>
+      db.using_statement(Running.table.select(sql = SQL.order_by(List(Running.name)))) { stmt =>
         List.from(
           stmt.execute_query().iterator { res =>
             val name = res.string(Running.name)
@@ -353,8 +353,8 @@
 
       if (delete.nonEmpty) {
         db.using_statement(
-          Running.table.delete() + SQL.where(Generic.sql_member(names = delete.map(_.job_name)))
-        )(_.execute())
+          Running.table.delete(
+            sql = SQL.where(Generic.sql_member(names = delete.map(_.job_name)))))(_.execute())
       }
 
       for (job <- insert) {
@@ -371,8 +371,7 @@
 
     def read_results(db: SQL.Database, names: List[String] = Nil): Map[String, Build_Job.Result] =
       db.using_statement(
-        Results.table.select() + if_proper(names, Results.name.where_member(names))
-      ) { stmt =>
+        Results.table.select(sql = if_proper(names, Results.name.where_member(names)))) { stmt =>
         Map.from(
           stmt.execute_query().iterator { res =>
             val name = res.string(Results.name)
@@ -395,9 +394,8 @@
       }
 
     def read_results_name(db: SQL.Database): Set[String] =
-      db.using_statement(Results.table.select(List(Results.name))) { stmt =>
-        Set.from(stmt.execute_query().iterator(_.string(Results.name)))
-      }
+      db.using_statement(Results.table.select(List(Results.name)))(stmt =>
+        Set.from(stmt.execute_query().iterator(_.string(Results.name))))
 
     def update_results(db: SQL.Database, results: Map[String, Build_Process.Result]): Boolean = {
       val old_results = read_results_name(db)
@@ -433,27 +431,26 @@
 
     def read_state(db: SQL.Database, instance: String): (Long, Int) =
       db.using_statement(
-        State.table.select() + SQL.where(Generic.sql_equal(instance = instance))
+        State.table.select(sql = SQL.where(Generic.sql_equal(instance = instance)))
       ) { stmt =>
-        (stmt.execute_query().iterator { res =>
-          val serial = res.long(State.serial)
-          val numa_index = res.int(State.numa_index)
-          (serial, numa_index)
-        }).nextOption.getOrElse(error("No build state instance " + instance + " in database " + db))
-      }
+          (stmt.execute_query().iterator { res =>
+            val serial = res.long(State.serial)
+            val numa_index = res.int(State.numa_index)
+            (serial, numa_index)
+          }).nextOption.getOrElse(error("No build state instance " + instance + " in database " + db))
+        }
 
-    def write_state(db: SQL.Database, instance: String, serial: Long, numa_index: Int): Unit = {
+    def write_state(db: SQL.Database, instance: String, serial: Long, numa_index: Int): Unit =
       db.using_statement(State.table.insert()) { stmt =>
         stmt.string(1) = instance
         stmt.long(2) = serial
         stmt.int(3) = numa_index
         stmt.execute()
       }
-    }
 
     def reset_state(db: SQL.Database, instance: String): Unit =
       db.using_statement(
-        State.table.delete() + SQL.where(Generic.sql_equal(instance = instance)))(_.execute())
+        State.table.delete(sql = SQL.where(Generic.sql_equal(instance = instance))))(_.execute())
 
     def init_database(db: SQL.Database, build_context: Build_Process.Context): Unit = {
       val tables =

--- a/src/Pure/Tools/server.scala	Sun Feb 26 19:18:24 2023 +0100
+++ b/src/Pure/Tools/server.scala	Sun Feb 26 20:19:01 2023 +0100
@@ -367,12 +367,13 @@
 
   def list(db: SQLite.Database): List[Info] =
     if (db.tables.contains(Data.table.name)) {
-      db.using_statement(Data.table.select())(stmt =>
+      db.using_statement(Data.table.select()) { stmt =>
         stmt.execute_query().iterator(res =>
           Info(
             res.string(Data.name),
             res.int(Data.port),
-            res.string(Data.password))).toList.sortBy(_.name))
+            res.string(Data.password))).toList.sortBy(_.name)
+      }
     }
     else Nil
 
@@ -390,8 +391,8 @@
         Isabelle_System.chmod("600", Data.database)
         db.create_table(Data.table)
         list(db).filterNot(_.active).foreach(server_info =>
-          db.using_statement(Data.table.delete(Data.name.where_equal(server_info.name)))(
-            _.execute()))
+          db.using_statement(
+            Data.table.delete(sql = Data.name.where_equal(server_info.name)))(_.execute()))
       }
       db.transaction {
         find(db, name) match {
@@ -402,7 +403,7 @@
             val server = new Server(port, log)
             val server_info = Info(name, server.port, server.password)
 
-            db.using_statement(Data.table.delete(Data.name.where_equal(name)))(_.execute())
+            db.using_statement(Data.table.delete(sql = Data.name.where_equal(name)))(_.execute())
             db.using_statement(Data.table.insert()) { stmt =>
               stmt.string(1) = server_info.name
               stmt.int(2) = server_info.port