tuned;
authorwenzelm
Fri, 05 May 2017 18:12:21 +0200
changeset 65731 393d34045ffb
parent 65730 7ae61e72a678
child 65732 7864aea16a87
tuned;
src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Fri May 05 17:20:50 2017 +0200
+++ b/src/Pure/General/sql.scala	Fri May 05 18:12:21 2017 +0200
@@ -46,7 +46,7 @@
     "SELECT " + (if (distinct) "DISTINCT " else "") + commas(columns.map(_.ident)) + " FROM "
 
   def join(table1: Table, table2: Table, sql: Source = "", outer: Boolean = false): Source =
-    table1.ident + (if (outer) " LEFT OUTER JOIN " else " INNER JOIN ") + table2.ident +
+    table1 + (if (outer) " LEFT OUTER JOIN " else " INNER JOIN ") + table2 +
       (if (sql == "") "" else " ON " + sql)
 
   def join_outer(table1: Table, table2: Table, sql: Source = ""): Source =
@@ -318,7 +318,7 @@
     def create_view(table: Table, strict: Boolean = false): Unit =
     {
       if (strict || !tables.contains(table.name)) {
-        val sql = "CREATE VIEW " + table.ident + " AS " + { table.query; table.body }
+        val sql = "CREATE VIEW " + table + " AS " + { table.query; table.body }
         using_statement(sql)(_.execute())
       }
     }