# HG changeset patch
# User wenzelm
# Date 1710185099 -3600
# Node ID ee4864e17c1173bb2a6cff240fa0d296f2448151
# Parent  819c28a7280f9fff2e1fb0ee5019f7e80e7f8843
tuned: prefer if_proper expression;

diff -r 819c28a7280f -r ee4864e17c11 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Mon Mar 11 15:07:02 2024 +0000
+++ b/src/Pure/General/sql.scala	Mon Mar 11 20:24:59 2024 +0100
@@ -49,10 +49,10 @@
   def enclosure(ss: Iterable[Source]): Source = ss.mkString("(", ", ", ")")
 
   def separate(sql: Source): Source =
-    (if (sql.isEmpty || sql.startsWith(" ")) "" else " ") + sql
+    if_proper(sql.nonEmpty && sql(0) != ' ', " ") + sql
 
   def select(columns: List[Column] = Nil, distinct: Boolean = false, sql: Source = ""): Source =
-    "SELECT " + (if (distinct) "DISTINCT " else "") +
+    "SELECT " + if_proper(distinct, "DISTINCT ") +
     (if (columns.isEmpty) "*" else commas(columns.map(_.ident))) + " FROM " + sql
 
   val join_outer: Source = " LEFT OUTER JOIN "
@@ -152,7 +152,7 @@
       else enclose(expr) + " AS " + SQL.ident(name)
 
     def decl(sql_type: Type => Source): Source =
-      ident + " " + sql_type(T) + (if (strict || primary_key) " NOT NULL" else "")
+      ident + " " + sql_type(T) + if_proper(strict || primary_key, " NOT NULL")
 
     def defined: String = ident + " IS NOT NULL"
     def undefined: String = ident + " IS NULL"
@@ -179,7 +179,7 @@
   }
 
   def order_by(columns: List[Column], descending: Boolean = false): Source =
-    " ORDER BY " + columns.mkString(", ") + (if (descending) " DESC" else "")
+    " ORDER BY " + columns.mkString(", ") + if_proper(descending, " DESC")
 
 
   /* tables */
@@ -577,7 +577,7 @@
       val escape = connection.getMetaData.getSearchStringEscape
       val pattern =
         name.iterator.map(c =>
-          (if (c == '_' || c == '%' || c == escape(0)) escape else "") + c).mkString
+          if_proper(c == '_' || c == '%' || c == escape(0), escape) + c).mkString
       get_tables(pattern = pattern).nonEmpty
     }