merged
authorwenzelm
Mon, 05 Sep 2016 15:00:37 +0200
changeset 63792 4ccb7e635477
parent 63787 ad2036bb81c6 (current diff)
parent 63791 c6cbdfaae19e (diff)
child 63793 e68a0b651eb5
merged
src/Pure/Tools/sql.scala
src/Pure/Tools/sqlite.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/sql.scala	Mon Sep 05 15:00:37 2016 +0200
@@ -0,0 +1,187 @@
+/*  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 + "`"
+  }
+
+  def enclosure(ss: Iterable[String]): String = ss.mkString("(", ", ", ")")
+
+
+  /* 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)
+    extends Function[ResultSet, A]
+  {
+    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: List[Column[Any]]): Table = new Table(name, columns)
+
+  class Table private[SQL](name: String, columns: List[Column[Any]])
+  {
+    private val columns_index: Map[String, Int] =
+      columns.iterator.map(_.name).zipWithIndex.toMap
+
+    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) + " " + enclosure(columns.map(_.sql_decl)) +
+        (if (rowid) "" else " WITHOUT ROWID")
+
+    def sql_drop(strict: Boolean): String =
+      "DROP TABLE " + (if (strict) "" else "IF EXISTS ") + quote_ident(name)
+
+    def sql_create_index(
+        index_name: String, index_columns: List[Column[Any]],
+        strict: Boolean, unique: Boolean): String =
+      "CREATE " + (if (unique) "UNIQUE " else "") + "INDEX " +
+        (if (strict) "" else "IF NOT EXISTS ") + quote_ident(index_name) + " ON " +
+        quote_ident(name) + " " + enclosure(index_columns.map(_.name))
+
+    def sql_drop_index(index_name: String, strict: Boolean): String =
+      "DROP INDEX " + (if (strict) "" else "IF EXISTS ") + quote_ident(index_name)
+
+    def sql_insert: String =
+      "INSERT INTO " + quote_ident(name) + " VALUES " + enclosure(columns.map(_ => "?"))
+
+    def sql_select(select_columns: List[Column[Any]], distinct: Boolean): String =
+      "SELECT " + (if (distinct) "DISTINCT " else "") +
+      commas(select_columns.map(_.sql_name)) + " FROM " + quote_ident(name)
+
+    override def toString: String =
+      "TABLE " + quote_ident(name) + " " + enclosure(columns.map(_.toString))
+  }
+
+
+  /* results */
+
+  def iterator[A](rs: ResultSet)(get: ResultSet => A): Iterator[A] = new Iterator[A]
+  {
+    private var _next: Boolean = rs.next()
+    def hasNext: Boolean = _next
+    def next: A = { val x = get(rs); _next = rs.next(); x }
+  }
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/sqlite.scala	Mon Sep 05 15:00:37 2016 +0200
@@ -0,0 +1,77 @@
+/*  Title:      Pure/General/sqlite.scala
+    Author:     Makarius
+
+Support for SQLite databases.
+*/
+
+package isabelle
+
+
+import java.sql.{DriverManager, Connection, PreparedStatement}
+
+
+object SQLite
+{
+  /** database connection **/
+
+  def open_database(path: Path): Database =
+  {
+    val path0 = path.expand
+    val s0 = File.platform_path(path0)
+    val s1 = if (Platform.is_windows) s0.replace('\\', '/') else s0
+    val connection = DriverManager.getConnection("jdbc:sqlite:" + s1)
+    new Database(path0, connection)
+  }
+
+  class Database private [SQLite](path: Path, val connection: Connection)
+  {
+    override def toString: String = path.toString
+
+    def close { connection.close }
+
+    def transaction[A](body: => A): A =
+    {
+      val auto_commit = connection.getAutoCommit
+      val savepoint = connection.setSavepoint
+
+      try {
+        connection.setAutoCommit(false)
+        val result = body
+        connection.commit
+        result
+      }
+      catch { case exn: Throwable => connection.rollback(savepoint); throw exn }
+      finally { connection.setAutoCommit(auto_commit) }
+    }
+
+
+    /* statements */
+
+    def statement(sql: String): PreparedStatement = connection.prepareStatement(sql)
+
+    def insert_statement(table: SQL.Table): PreparedStatement = statement(table.sql_insert)
+
+    def select_statement(table: SQL.Table, columns: List[SQL.Column[Any]],
+        sql: String = "", distinct: Boolean = false): PreparedStatement =
+      statement(table.sql_select(columns, distinct) + (if (sql == "") "" else " " + sql))
+
+
+    /* tables */
+
+    def tables: List[String] =
+      SQL.iterator(connection.getMetaData.getTables(null, null, "%", null))(_.getString(3)).toList
+
+    def create_table(table: SQL.Table, strict: Boolean = true, rowid: Boolean = true): Unit =
+      using(statement(table.sql_create(strict, rowid)))(_.execute())
+
+    def drop_table(table: SQL.Table, strict: Boolean = true): Unit =
+      using(statement(table.sql_drop(strict)))(_.execute())
+
+    def create_index(table: SQL.Table, name: String, columns: List[SQL.Column[Any]],
+        strict: Boolean = true, unique: Boolean = false): Unit =
+      using(statement(table.sql_create_index(name, columns, strict, unique)))(_.execute())
+
+    def drop_index(table: SQL.Table, name: String, strict: Boolean = true): Unit =
+      using(statement(table.sql_drop_index(name, strict)))(_.execute())
+  }
+}
--- a/src/Pure/ROOT.scala	Mon Sep 05 13:09:18 2016 +0200
+++ b/src/Pure/ROOT.scala	Mon Sep 05 15:00:37 2016 +0200
@@ -11,6 +11,7 @@
   val error = Exn.error _
   val cat_error = Exn.cat_error _
 
+  def using[A <: { def close() }, B](x: A)(f: A => B): B = Library.using(x)(f)
   val space_explode = Library.space_explode _
   val split_lines = Library.split_lines _
   val cat_lines = Library.cat_lines _
--- a/src/Pure/Tools/sql.scala	Mon Sep 05 13:09:18 2016 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,154 +0,0 @@
-/*  Title:      Pure/Tools/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("(", ", ", ")")
-  }
-}
--- a/src/Pure/Tools/sqlite.scala	Mon Sep 05 13:09:18 2016 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,71 +0,0 @@
-/*  Title:      Pure/Tools/sqlite.scala
-    Author:     Makarius
-
-Support for SQLite databases.
-*/
-
-package isabelle
-
-
-import java.sql.{DriverManager, Connection, PreparedStatement}
-
-
-object SQLite
-{
-  /** database connection **/
-
-  class Database private [SQLite](path: Path, val connection: Connection)
-  {
-    override def toString: String = path.toString
-
-    def close { connection.close }
-
-    def transaction[A](body: => A): A =
-    {
-      val auto_commit = connection.getAutoCommit
-      val savepoint = connection.setSavepoint
-
-      try {
-        connection.setAutoCommit(false)
-        val result = body
-        connection.commit
-        result
-      }
-      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
-    val s0 = File.platform_path(path0)
-    val s1 = if (Platform.is_windows) s0.replace('\\', '/') else s0
-    val connection = DriverManager.getConnection("jdbc:sqlite:" + s1)
-    new Database(path0, connection)
-  }
-
-  def with_database[A](path: Path)(body: Database => A): A =
-  {
-    val db = open_database(path)
-    try { body(db) } finally { db.close }
-  }
-}
--- a/src/Pure/build-jars	Mon Sep 05 13:09:18 2016 +0200
+++ b/src/Pure/build-jars	Mon Sep 05 15:00:37 2016 +0200
@@ -43,6 +43,8 @@
   General/properties.scala
   General/scan.scala
   General/sha1.scala
+  General/sql.scala
+  General/sqlite.scala
   General/symbol.scala
   General/time.scala
   General/timing.scala
@@ -116,8 +118,6 @@
   Tools/news.scala
   Tools/print_operation.scala
   Tools/simplifier_trace.scala
-  Tools/sql.scala
-  Tools/sqlite.scala
   Tools/task_statistics.scala
   Tools/update_cartouches.scala
   Tools/update_header.scala
--- a/src/Pure/library.scala	Mon Sep 05 13:09:18 2016 +0200
+++ b/src/Pure/library.scala	Mon Sep 05 15:00:37 2016 +0200
@@ -15,6 +15,15 @@
 
 object Library
 {
+  /* resource management */
+
+  def using[A <: { def close() }, B](x: A)(f: A => B): B =
+  {
+    try { f(x) }
+    finally { if (x != null) x.close() }
+  }
+
+
   /* integers */
 
   private val small_int = 10000