src/Pure/General/sql.scala
changeset 65780 8baf789b1537
parent 65778 666a1bac126b
child 65804 73ed0ebac3b0
--- 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 "")