# HG changeset patch
# User wenzelm
# Date 1494268019 -7200
# Node ID 8baf789b15372ecf19f96b32c35de60a88bd9073
# Parent  a42c9e375405c36802bd272fc4a2b023c8d51257
allow column with defining expression;

diff -r a42c9e375405 -r 8baf789b1537 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Mon May 08 17:33:46 2017 +0200
+++ b/src/Pure/General/sql.scala	Mon May 08 20:26:59 2017 +0200
@@ -99,12 +99,15 @@
   }
 
   sealed case class Column(
-    name: String, T: Type.Value, strict: Boolean = false, primary_key: Boolean = false)
+    name: String, T: Type.Value, strict: Boolean = false, primary_key: Boolean = false,
+    expr: SQL.Source = "")
   {
     def apply(table: Table): Column =
       Column(Long_Name.qualify(table.name, name), T, strict = strict, primary_key = primary_key)
 
-    def ident: Source = SQL.ident(name)
+    def ident: Source =
+      if (expr == "") SQL.ident(name)
+      else enclose(expr) + " AS " + SQL.ident(name)
 
     def decl(sql_type: Type.Value => Source): Source =
       ident + " " + sql_type(T) + (if (strict || primary_key) " NOT NULL" else "")