# HG changeset patch
# User wenzelm
# Date 1489930997 -3600
# Node ID 981df08de0ab03fa7730376c1a91b9d893c402f1
# Parent  1964d3cb2e5789932066a4aedc10b8678932b697
more general primary_key;

diff -r 1964d3cb2e57 -r 981df08de0ab src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Sun Mar 19 14:06:45 2017 +0100
+++ b/src/Pure/General/sql.scala	Sun Mar 19 14:43:17 2017 +0100
@@ -89,9 +89,7 @@
   {
     def sql_name: String = quote_ident(name)
     def sql_decl(sql_type: Type.Value => String): String =
-      sql_name + " " + sql_type(T) +
-      (if (strict) " NOT NULL" else "") +
-      (if (primary_key) " PRIMARY KEY" else "")
+      sql_name + " " + sql_type(T) + (if (strict || primary_key) " NOT NULL" else "")
 
     override def toString: String = sql_decl(sql_type_default)
   }
@@ -109,16 +107,19 @@
       case bad => error("Duplicate column names " + commas_quote(bad) + " for table " + quote(name))
     }
 
-    columns.filter(_.primary_key) match {
-      case bad if bad.length > 1 =>
-        error("Multiple primary keys " + commas_quote(bad.map(_.name)) + " for table " + quote(name))
-      case _ =>
+    def sql_columns(sql_type: Type.Value => String): String =
+    {
+      val primary_key =
+        columns.filter(_.primary_key).map(_.name) match {
+          case Nil => Nil
+          case keys => List("PRIMARY KEY " + enclosure(keys))
+        }
+      enclosure(columns.map(_.sql_decl(sql_type)) ::: primary_key)
     }
 
     def sql_create(strict: Boolean, rowid: Boolean, sql_type: Type.Value => String): String =
       "CREATE TABLE " + (if (strict) "" else "IF NOT EXISTS ") +
-        quote_ident(name) + " " + enclosure(columns.map(_.sql_decl(sql_type))) +
-        (if (rowid) "" else " WITHOUT ROWID")
+        quote_ident(name) + " " + sql_columns(sql_type) + (if (rowid) "" else " WITHOUT ROWID")
 
     def sql_drop(strict: Boolean): String =
       "DROP TABLE " + (if (strict) "" else "IF EXISTS ") + quote_ident(name)
@@ -144,7 +145,7 @@
       commas(select_columns.map(_.sql_name)) + " FROM " + quote_ident(name)
 
     override def toString: String =
-      "TABLE " + quote_ident(name) + " " + enclosure(columns.map(_.toString))
+      "TABLE " + quote_ident(name) + " " + sql_columns(sql_type_default)
   }