--- /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("(", ", ", ")")
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/sqlite.scala Mon Sep 05 10:34:45 2016 +0200
@@ -0,0 +1,71 @@
+/* Title: Pure/General/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/Tools/sql.scala Sun Sep 04 23:04:34 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 Sun Sep 04 23:04:34 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 Sun Sep 04 23:04:34 2016 +0200
+++ b/src/Pure/build-jars Mon Sep 05 10:34:45 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