# HG changeset patch
# User wenzelm
# Date 1493652505 -7200
# Node ID d2f19b4a16ae1b1fe0fc8671079006d947fc54cc
# Parent  366bc4e6a238768d97669f54eb0391a1e0c11b30
support for views;

diff -r 366bc4e6a238 -r d2f19b4a16ae src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Mon May 01 15:42:26 2017 +0200
+++ b/src/Pure/General/sql.scala	Mon May 01 17:28:25 2017 +0200
@@ -78,6 +78,11 @@
 
   /* columns */
 
+  trait Qualifier
+  {
+    def name: String
+  }
+
   object Column
   {
     def bool(name: String, strict: Boolean = false, primary_key: Boolean = false): Column =
@@ -99,8 +104,8 @@
   sealed case class Column(
     name: String, T: Type.Value, strict: Boolean = false, primary_key: Boolean = false)
   {
-    def apply(table: Table): Column =
-      Column(Long_Name.qualify(table.name, name), T, strict = strict, primary_key = primary_key)
+    def apply(qual: Qualifier): Column =
+      Column(Long_Name.qualify(qual.name, name), T, strict = strict, primary_key = primary_key)
 
     def sql: String = ident(name)
     def sql_decl(sql_type: Type.Value => String): String =
@@ -115,7 +120,7 @@
 
   /* tables */
 
-  sealed case class Table(name: String, columns: List[Column])
+  sealed case class Table(name: String, columns: List[Column]) extends Qualifier
   {
     private val columns_index: Map[String, Int] =
       columns.iterator.map(_.name).zipWithIndex.toMap
@@ -168,6 +173,16 @@
   }
 
 
+  /* views */
+
+  sealed case class View(name: String, columns: List[Column]) extends Qualifier
+  {
+    def sql: String = ident(name)
+    def sql_create(query: String): String = "CREATE VIEW " + ident(name) + " AS " + query
+    override def toString: String =
+      "VIEW " + ident(name) + " " + enclosure(columns.map(_.sql_decl(sql_type_default)))
+  }
+
 
   /** SQL database operations **/
 
@@ -296,7 +311,7 @@
     }
 
 
-    /* tables */
+    /* tables and views */
 
     def tables: List[String] =
       iterator(connection.getMetaData.getTables(null, null, "%", null))(_.getString(3)).toList
@@ -314,6 +329,9 @@
 
     def drop_index(table: Table, name: String, strict: Boolean = false): Unit =
       using(statement(table.sql_drop_index(name, strict)))(_.execute())
+
+    def create_view(view: View, query: String): Unit =
+      using(statement(view.sql_create(query)))(_.execute())
   }
 }