# HG changeset patch # User wenzelm # Date 1473064485 -7200 # Node ID 3160826b92f889b271c523e3966898aad4ce6ff8 # Parent b948c4f92b88fb35e638059897fccd2e789c9171 clarified modules; 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("(", ", ", ")") + } +} diff -r b948c4f92b88 -r 3160826b92f8 src/Pure/General/sqlite.scala --- /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 } + } +} diff -r b948c4f92b88 -r 3160826b92f8 src/Pure/Tools/sql.scala --- 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("(", ", ", ")") - } -} diff -r b948c4f92b88 -r 3160826b92f8 src/Pure/Tools/sqlite.scala --- 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 } - } -} diff -r b948c4f92b88 -r 3160826b92f8 src/Pure/build-jars --- 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