# HG changeset patch # User wenzelm # Date 1486669661 -3600 # Node ID 86308845aa4386c89fbcd200fbb91b93e34009c7 # Parent 14641ca387f8c622d83a285346e316abcbbc4d73 tuned; diff -r 14641ca387f8 -r 86308845aa43 src/Pure/General/sql.scala --- a/src/Pure/General/sql.scala Thu Feb 09 16:58:27 2017 +0100 +++ b/src/Pure/General/sql.scala Thu Feb 09 20:47:41 2017 +0100 @@ -52,7 +52,16 @@ } type Type_Name = Type.Value => String - def default_type_name(t: Type.Value): String = t.toString + + def type_name_default(t: Type.Value): String = t.toString + + def type_name_sqlite(t: Type.Value): String = + if (t == Type.Boolean) "INTEGER" + else type_name_default(t) + + def type_name_postgresql(t: Type.Value): String = + if (t == Type.Bytes) "BYTEA" + else type_name_default(t) /* columns */ @@ -97,7 +106,7 @@ if (rs.wasNull) None else Some(x) } - override def toString: String = sql_decl(default_type_name) + override def toString: String = sql_decl(type_name_default) } class Column_Boolean private[SQL](name: String, strict: Boolean, primary_key: Boolean) @@ -286,9 +295,7 @@ { override def toString: String = name - def type_name(t: SQL.Type.Value): String = - if (t == SQL.Type.Boolean) "INTEGER" - else SQL.default_type_name(t) + def type_name(t: SQL.Type.Value): String = SQL.type_name_sqlite(t) def rebuild { using(statement("VACUUM"))(_.execute()) } } @@ -342,9 +349,7 @@ { override def toString: String = name - def type_name(t: SQL.Type.Value): String = - if (t == SQL.Type.Bytes) "BYTEA" - else SQL.default_type_name(t) + def type_name(t: SQL.Type.Value): String = SQL.type_name_postgresql(t) override def close() { super.close; port_forwarding.foreach(_.close) } }