# HG changeset patch
# User wenzelm
# Date 1489931437 -3600
# Node ID e886aed88b2cc1c3f947418f557c8fa9b19ddcfc
# Parent  cb7cb57c7ce166b8b74cbf39feef1fb7f4645572
clarified signature: rowid is specific to SQLite;

diff -r cb7cb57c7ce1 -r e886aed88b2c src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Sun Mar 19 14:43:54 2017 +0100
+++ b/src/Pure/General/sql.scala	Sun Mar 19 14:50:37 2017 +0100
@@ -117,9 +117,9 @@
       enclosure(columns.map(_.sql_decl(sql_type)) ::: primary_key)
     }
 
-    def sql_create(strict: Boolean, rowid: Boolean, sql_type: Type.Value => String): String =
+    def sql_create(strict: Boolean, sql_type: Type.Value => String): String =
       "CREATE TABLE " + (if (strict) "" else "IF NOT EXISTS ") +
-        quote_ident(name) + " " + sql_columns(sql_type) + (if (rowid) "" else " WITHOUT ROWID")
+        quote_ident(name) + " " + sql_columns(sql_type)
 
     def sql_drop(strict: Boolean): String =
       "DROP TABLE " + (if (strict) "" else "IF EXISTS ") + quote_ident(name)
@@ -255,8 +255,9 @@
     def tables: List[String] =
       iterator(connection.getMetaData.getTables(null, null, "%", null))(_.getString(3)).toList
 
-    def create_table(table: Table, strict: Boolean = false, rowid: Boolean = true): Unit =
-      using(statement(table.sql_create(strict, rowid, sql_type)))(_.execute())
+    def create_table(table: Table, strict: Boolean = false, sql: String = ""): Unit =
+      using(statement(table.sql_create(strict, sql_type) + (if (sql == "") "" else " " + sql)))(
+        _.execute())
 
     def drop_table(table: Table, strict: Boolean = false): Unit =
       using(statement(table.sql_drop(strict)))(_.execute())