# HG changeset patch
# User wenzelm
# Date 1486655791 -3600
# Node ID 42bffd1637f016d14631b1899b1d184c5ccfdd01
# Parent  a27e9908dcf794cb8caee6865aaa84f6f2c581e2
support for type Boolean;

diff -r a27e9908dcf7 -r 42bffd1637f0 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Thu Feb 09 16:06:45 2017 +0100
+++ b/src/Pure/General/sql.scala	Thu Feb 09 16:56:31 2017 +0100
@@ -43,6 +43,7 @@
 
   object Type extends Enumeration
   {
+    val Boolean = Value("BOOLEAN")
     val Int = Value("INTEGER")
     val Long = Value("BIGINT")
     val Double = Value("DOUBLE PRECISION")
@@ -58,6 +59,8 @@
 
   object Column
   {
+    def bool(name: String, strict: Boolean = true, primary_key: Boolean = false): Column[Boolean] =
+      new Column_Boolean(name, strict, primary_key)
     def int(name: String, strict: Boolean = true, primary_key: Boolean = false): Column[Int] =
       new Column_Int(name, strict, primary_key)
     def long(name: String, strict: Boolean = true, primary_key: Boolean = false): Column[Long] =
@@ -97,6 +100,12 @@
     override def toString: String = sql_decl(default_type_name)
   }
 
+  class Column_Boolean private[SQL](name: String, strict: Boolean, primary_key: Boolean)
+    extends Column[Boolean](name, strict, primary_key, Type.Boolean)
+  {
+    def apply(rs: ResultSet): Boolean = rs.getBoolean(name)
+  }
+
   class Column_Int private[SQL](name: String, strict: Boolean, primary_key: Boolean)
     extends Column[Int](name, strict, primary_key, Type.Int)
   {
@@ -203,7 +212,7 @@
   {
     /* types */
 
-    def type_name(t: Type.Value): String = default_type_name(t)
+    def type_name(t: Type.Value): String
 
 
     /* connection */
@@ -278,6 +287,10 @@
   {
     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 rebuild { using(statement("VACUUM"))(_.execute()) }
   }
 }
@@ -330,7 +343,7 @@
   {
     override def toString: String = name
 
-    override def type_name(t: SQL.Type.Value): String =
+    def type_name(t: SQL.Type.Value): String =
       if (t == SQL.Type.Bytes) "BYTEA"
       else SQL.default_type_name(t)