# HG changeset patch
# User wenzelm
# Date 1494000741 -7200
# Node ID 393d34045ffb4357b23cc79909acde95c37e4a90
# Parent  7ae61e72a678057e95bc176c977d414c2353a2fd
tuned;

diff -r 7ae61e72a678 -r 393d34045ffb 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())
       }
     }