diff -r b948c4f92b88 -r 3160826b92f8 src/Pure/General/sql.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/sql.scala	Mon Sep 05 10:34:45 2016 +0200
@@ -0,0 +1,154 @@
+/*  Title:      Pure/General/sql.scala
+    Author:     Makarius
+
+Generic support for SQL.
+*/
+
+package isabelle
+
+
+import java.sql.ResultSet
+
+
+object SQL
+{
+  /* concrete syntax */
+
+  def quote_char(c: Char): String =
+    c match {
+      case '\u0000' => "\\0"
+      case '\'' => "\\'"
+      case '\"' => "\\\""
+      case '\b' => "\\b"
+      case '\n' => "\\n"
+      case '\r' => "\\r"
+      case '\t' => "\\t"
+      case '\u001a' => "\\Z"
+      case '\\' => "\\\\"
+      case _ => c.toString
+    }
+
+  def quote_string(s: String): String =
+    quote(s.map(quote_char(_)).mkString)
+
+  def quote_ident(s: String): String =
+  {
+    require(!s.contains('`'))
+    "`" + s + "`"
+  }
+
+
+  /* columns */
+
+  object Column
+  {
+    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] =
+      new Column_Long(name, strict, primary_key)
+    def double(name: String, strict: Boolean = true, primary_key: Boolean = false): Column[Double] =
+      new Column_Double(name, strict, primary_key)
+    def string(name: String, strict: Boolean = true, primary_key: Boolean = false): Column[String] =
+      new Column_String(name, strict, primary_key)
+    def bytes(name: String, strict: Boolean = true, primary_key: Boolean = false): Column[Bytes] =
+      new Column_Bytes(name, strict, primary_key)
+  }
+
+  abstract class Column[+A] private[SQL](
+    val name: String, val strict: Boolean, val primary_key: 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 "") +
+      (if (primary_key) " PRIMARY KEY" else "")
+
+    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
+  }
+
+  class Column_Int private[SQL](name: String, strict: Boolean, primary_key: Boolean)
+    extends Column[Int](name, strict, primary_key)
+  {
+    def sql_type: String = "INTEGER"
+    def apply(rs: ResultSet): Int = rs.getInt(name)
+  }
+
+  class Column_Long private[SQL](name: String, strict: Boolean, primary_key: Boolean)
+    extends Column[Long](name, strict, primary_key)
+  {
+    def sql_type: String = "INTEGER"
+    def apply(rs: ResultSet): Long = rs.getLong(name)
+  }
+
+  class Column_Double private[SQL](name: String, strict: Boolean, primary_key: Boolean)
+    extends Column[Double](name, strict, primary_key)
+  {
+    def sql_type: String = "REAL"
+    def apply(rs: ResultSet): Double = rs.getDouble(name)
+  }
+
+  class Column_String private[SQL](name: String, strict: Boolean, primary_key: Boolean)
+    extends Column[String](name, strict, primary_key)
+  {
+    def sql_type: String = "TEXT"
+    def apply(rs: ResultSet): String =
+    {
+      val s = rs.getString(name)
+      if (s == null) "" else s
+    }
+  }
+
+  class Column_Bytes private[SQL](name: String, strict: Boolean, primary_key: Boolean)
+    extends Column[Bytes](name, strict, primary_key)
+  {
+    def sql_type: String = "BLOB"
+    def apply(rs: ResultSet): Bytes =
+    {
+      val bs = rs.getBytes(name)
+      if (bs == null) Bytes.empty else Bytes(bs)
+    }
+  }
+
+
+  /* tables */
+
+  def table(name: String, columns: Column[Any]*): Table = new Table(name, columns.toList)
+
+  class Table private[SQL](name: String, columns: List[Column[Any]])
+  {
+    Library.duplicates(columns.map(_.name)) match {
+      case Nil =>
+      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_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)
+
+    override def toString: String =
+      "TABLE " + quote_ident(name) + " " + columns.map(_.toString).mkString("(", ", ", ")")
+  }
+}