src/Pure/General/sql.scala

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