# HG changeset patch
# User wenzelm
# Date 1473013883 -7200
# Node ID 163244cefb4e1ef6d5c9d8faa13d3d3690bf8326
# Parent  9da65bc756100ee43c008d23837f0edcfca3f4c1
more operations;
clarified NULL treatment;

diff -r 9da65bc75610 -r 163244cefb4e src/Pure/Tools/sql.scala
--- a/src/Pure/Tools/sql.scala	Sun Sep 04 17:38:22 2016 +0200
+++ b/src/Pure/Tools/sql.scala	Sun Sep 04 20:31:23 2016 +0200
@@ -49,13 +49,22 @@
     def bytes(name: String, strict: Boolean = true): Column[Bytes] = new Column_Bytes(name, strict)
   }
 
-  abstract class Column[A] private[SQL](val name: String, val strict: Boolean)
+  abstract class Column[+A] private[SQL](val name: String, val strict: Boolean)
   {
     def sql_name: String = quote_ident(name)
     def sql_type: String
     def sql_decl: String = sql_name + " " + sql_type + (if (strict) " NOT NULL" else "")
-    def result(rs: ResultSet): A
-    def result_string(rs: ResultSet): String = rs.getString(name)
+    def string(rs: ResultSet): String =
+    {
+      val s = rs.getString(name)
+      if (s == null) "" else s
+    }
+    def apply(rs: ResultSet): A
+    def get(rs: ResultSet): Option[A] =
+    {
+      val x = apply(rs)
+      if (rs.wasNull) None else Some(x)
+    }
 
     override def toString: String = sql_decl
   }
@@ -64,38 +73,56 @@
     extends Column[Int](name, strict)
   {
     def sql_type: String = "INTEGER"
-    def result(rs: ResultSet): Int = rs.getInt(name)
+    def apply(rs: ResultSet): Int = rs.getInt(name)
   }
 
   class Column_Long private[SQL](name: String, strict: Boolean)
     extends Column[Long](name, strict)
   {
     def sql_type: String = "INTEGER"
-    def result(rs: ResultSet): Long = rs.getLong(name)
+    def apply(rs: ResultSet): Long = rs.getLong(name)
   }
 
   class Column_Double private[SQL](name: String, strict: Boolean)
     extends Column[Double](name, strict)
   {
     def sql_type: String = "REAL"
-    def result(rs: ResultSet): Double = rs.getDouble(name)
+    def apply(rs: ResultSet): Double = rs.getDouble(name)
   }
 
   class Column_String private[SQL](name: String, strict: Boolean)
     extends Column[String](name, strict)
   {
     def sql_type: String = "TEXT"
-    def result(rs: ResultSet): String = rs.getString(name)
+    def apply(rs: ResultSet): String =
+    {
+      val s = rs.getString(name)
+      if (s == null) "" else s
+    }
   }
 
   class Column_Bytes private[SQL](name: String, strict: Boolean)
     extends Column[Bytes](name, strict)
   {
     def sql_type: String = "BLOB"
-    def result(rs: ResultSet): Bytes =
+    def apply(rs: ResultSet): Bytes =
     {
       val bs = rs.getBytes(name)
-      if (bs == null) null else Bytes(bs)
+      if (bs == null) Bytes.empty else Bytes(bs)
     }
   }
+
+
+  /* tables */
+
+  sealed case class Table(name: String, columns: Column[Any]*)
+  {
+    def sql_create(strict: Boolean, rowid: Boolean): String =
+      "CREATE TABLE " + (if (strict) "" else " IF NOT EXISTS ") +
+        quote_ident(name) + " " + columns.map(_.sql_decl).mkString("(", ", ", ")") +
+        (if (rowid) "" else " WITHOUT ROWID")
+
+    def sql_drop(strict: Boolean): String =
+      "DROP TABLE " + (if (strict) "" else " IF EXISTS ") + quote_ident(name)
+  }
 }
diff -r 9da65bc75610 -r 163244cefb4e src/Pure/Tools/sqlite.scala
--- a/src/Pure/Tools/sqlite.scala	Sun Sep 04 17:38:22 2016 +0200
+++ b/src/Pure/Tools/sqlite.scala	Sun Sep 04 20:31:23 2016 +0200
@@ -7,12 +7,12 @@
 package isabelle
 
 
-import java.sql.{Connection, DriverManager}
+import java.sql.{DriverManager, Connection, PreparedStatement}
 
 
 object SQLite
 {
-  /* database connection */
+  /** database connection **/
 
   class Database private [SQLite](path: Path, val connection: Connection)
   {
@@ -34,8 +34,26 @@
       catch { case exn: Throwable => connection.rollback(savepoint); throw exn }
       finally { connection.setAutoCommit(auto_commit) }
     }
+
+    def with_statement[A](sql: String)(body: PreparedStatement => A): A =
+    {
+      val stmt = connection.prepareStatement(sql)
+      try { body(stmt) } finally { stmt.close }
+    }
+
+
+    /* tables */
+
+    def create_table(table: SQL.Table, strict: Boolean = true, rowid: Boolean = true): Unit =
+      with_statement(table.sql_create(strict, rowid))(_.execute())
+
+    def drop_table(table: SQL.Table, strict: Boolean = true): Unit =
+      with_statement(table.sql_drop(strict))(_.execute())
   }
 
+
+  /* open database */
+
   def open_database(path: Path): Database =
   {
     val path0 = path.expand