# HG changeset patch
# User wenzelm
# Date 1677526240 -3600
# Node ID be8e14c7da800da0618b48fd115bc274aeee3f4a
# Parent  907b2cad365ace6e15f0b7020c3a05c410285740
clarified signature, although "sql" argument is de-facto mandatory;

diff -r 907b2cad365a -r be8e14c7da80 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Mon Feb 27 20:25:10 2023 +0100
+++ b/src/Pure/Admin/build_log.scala	Mon Feb 27 20:30:40 2023 +0100
@@ -1083,7 +1083,7 @@
         else (columns1, table1.ident)
 
       val sessions =
-        db.using_statement(SQL.select(columns) + from + where) { stmt =>
+        db.using_statement(SQL.select(columns, sql = from + where)) { stmt =>
           stmt.execute_query().iterator({ res =>
             val session_name = res.string(Data.session_name)
             val session_entry =
diff -r 907b2cad365a -r be8e14c7da80 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Mon Feb 27 20:25:10 2023 +0100
+++ b/src/Pure/General/sql.scala	Mon Feb 27 20:30:40 2023 +0100
@@ -50,9 +50,9 @@
   def separate(sql: Source): Source =
     (if (sql.isEmpty || sql.startsWith(" ")) "" else " ") + sql
 
-  def select(columns: List[Column] = Nil, distinct: Boolean = false): Source =
+  def select(columns: List[Column] = Nil, distinct: Boolean = false, sql: Source = ""): Source =
     "SELECT " + (if (distinct) "DISTINCT " else "") +
-    (if (columns.isEmpty) "*" else commas(columns.map(_.ident))) + " FROM "
+    (if (columns.isEmpty) "*" else commas(columns.map(_.ident))) + " FROM " + sql
 
   val join_outer: Source = " LEFT OUTER JOIN "
   val join_inner: Source = " INNER JOIN "
@@ -203,7 +203,7 @@
       select_columns: List[Column] = Nil,
       distinct: Boolean = false,
       sql: Source = ""
-    ): Source = SQL.select(select_columns, distinct = distinct) + ident + SQL.separate(sql)
+    ): Source = SQL.select(select_columns, distinct = distinct, sql = ident + SQL.separate(sql))
 
     override def toString: Source = ident
   }