# HG changeset patch
# User wenzelm
# Date 1710185629 -3600
# Node ID c49cb2a1ec44369a61fc1509ded781ee33f1b464
# Parent  bc979e334c7dfe6726e07f8b444c98dbdd1bffec
tuned: prefer if_proper expression;

diff -r bc979e334c7d -r c49cb2a1ec44 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Mon Mar 11 20:31:35 2024 +0100
+++ b/src/Pure/General/sql.scala	Mon Mar 11 20:33:49 2024 +0100
@@ -148,8 +148,7 @@
       Column(Long_Name.qualify(table.name, name), T, strict = strict, primary_key = primary_key)
 
     def ident: Source =
-      if (expr == "") SQL.ident(name)
-      else enclose(expr) + " AS " + SQL.ident(name)
+      if_proper(expr, enclose(expr) + " AS ") + SQL.ident(name)
 
     def decl(sql_type: Type => Source): Source =
       ident + " " + sql_type(T) + if_proper(strict || primary_key, " NOT NULL")