src/Pure/Tools/sql.scala

 /*  Title:      Pure/Tools/sql.scala
     Author:     Makarius
 
-Support for SQL.
+Generic support for SQL.
 */
 
 package isabelle
+
+
+import java.sql.ResultSet
 
 
 object SQL
 {
   /* concrete syntax */

     }
 
   def quote_string(s: String): String =
     quote(s.map(quote_char(_)).mkString)
 
-  def quote_ident(s: String): String = "`" + s + "`"
+  def quote_ident(s: String): String =
+  {
+    require(!s.contains('`'))
+    "`" + s + "`"
+  }
+
+
+  /* columns */
+
+  object Column
+  {
+    def int(name: String, strict: Boolean = true): Column[Int] = new Column_Int(name, strict)
+    def long(name: String, strict: Boolean = true): Column[Long] = new Column_Long(name, strict)
+    def double(name: String, strict: Boolean = true): Column[Double] = new Column_Double(name, strict)
+    def string(name: String, strict: Boolean = true): Column[String] = new Column_String(name, strict)
+    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)
+  {
+    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)
+
+    override def toString: String = sql_decl
+  }
+
+  class Column_Int private[SQL](name: String, strict: Boolean)
+    extends Column[Int](name, strict)
+  {
+    def sql_type: String = "INTEGER"
+    def result(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)
+  }
+
+  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)
+  }
+
+  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)
+  }
+
+  class Column_Bytes private[SQL](name: String, strict: Boolean)
+    extends Column[Bytes](name, strict)
+  {
+    def sql_type: String = "BLOB"
+    def result(rs: ResultSet): Bytes =
+    {
+      val bs = rs.getBytes(name)
+      if (bs == null) null else Bytes(bs)
+    }
+  }
 }