more general primary_key;
authorwenzelm
Sun Mar 19 14:43:17 2017 +0100 (2017-03-19)
changeset 65325981df08de0ab
parent 65324 1964d3cb2e57
child 65326 cb7cb57c7ce1
more general primary_key;
src/Pure/General/sql.scala
     1.1 --- a/src/Pure/General/sql.scala	Sun Mar 19 14:06:45 2017 +0100
     1.2 +++ b/src/Pure/General/sql.scala	Sun Mar 19 14:43:17 2017 +0100
     1.3 @@ -89,9 +89,7 @@
     1.4    {
     1.5      def sql_name: String = quote_ident(name)
     1.6      def sql_decl(sql_type: Type.Value => String): String =
     1.7 -      sql_name + " " + sql_type(T) +
     1.8 -      (if (strict) " NOT NULL" else "") +
     1.9 -      (if (primary_key) " PRIMARY KEY" else "")
    1.10 +      sql_name + " " + sql_type(T) + (if (strict || primary_key) " NOT NULL" else "")
    1.11  
    1.12      override def toString: String = sql_decl(sql_type_default)
    1.13    }
    1.14 @@ -109,16 +107,19 @@
    1.15        case bad => error("Duplicate column names " + commas_quote(bad) + " for table " + quote(name))
    1.16      }
    1.17  
    1.18 -    columns.filter(_.primary_key) match {
    1.19 -      case bad if bad.length > 1 =>
    1.20 -        error("Multiple primary keys " + commas_quote(bad.map(_.name)) + " for table " + quote(name))
    1.21 -      case _ =>
    1.22 +    def sql_columns(sql_type: Type.Value => String): String =
    1.23 +    {
    1.24 +      val primary_key =
    1.25 +        columns.filter(_.primary_key).map(_.name) match {
    1.26 +          case Nil => Nil
    1.27 +          case keys => List("PRIMARY KEY " + enclosure(keys))
    1.28 +        }
    1.29 +      enclosure(columns.map(_.sql_decl(sql_type)) ::: primary_key)
    1.30      }
    1.31  
    1.32      def sql_create(strict: Boolean, rowid: Boolean, sql_type: Type.Value => String): String =
    1.33        "CREATE TABLE " + (if (strict) "" else "IF NOT EXISTS ") +
    1.34 -        quote_ident(name) + " " + enclosure(columns.map(_.sql_decl(sql_type))) +
    1.35 -        (if (rowid) "" else " WITHOUT ROWID")
    1.36 +        quote_ident(name) + " " + sql_columns(sql_type) + (if (rowid) "" else " WITHOUT ROWID")
    1.37  
    1.38      def sql_drop(strict: Boolean): String =
    1.39        "DROP TABLE " + (if (strict) "" else "IF EXISTS ") + quote_ident(name)
    1.40 @@ -144,7 +145,7 @@
    1.41        commas(select_columns.map(_.sql_name)) + " FROM " + quote_ident(name)
    1.42  
    1.43      override def toString: String =
    1.44 -      "TABLE " + quote_ident(name) + " " + enclosure(columns.map(_.toString))
    1.45 +      "TABLE " + quote_ident(name) + " " + sql_columns(sql_type_default)
    1.46    }
    1.47  
    1.48