# HG changeset patch # User wenzelm # Date 1473080437 -7200 # Node ID 4ccb7e6354772c062c60676fd3af2d686552a402 # Parent ad2036bb81c674079d53ea849685045e4a08b557# Parent c6cbdfaae19eb24acbf2a031a96173728996969a merged diff -r ad2036bb81c6 -r 4ccb7e635477 src/Pure/General/sql.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 } + } +} diff -r ad2036bb81c6 -r 4ccb7e635477 src/Pure/General/sqlite.scala --- /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()) + } +} diff -r ad2036bb81c6 -r 4ccb7e635477 src/Pure/ROOT.scala --- 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 _ diff -r ad2036bb81c6 -r 4ccb7e635477 src/Pure/Tools/sql.scala --- 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("(", ", ", ")") - } -} diff -r ad2036bb81c6 -r 4ccb7e635477 src/Pure/Tools/sqlite.scala --- 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 } - } -} diff -r ad2036bb81c6 -r 4ccb7e635477 src/Pure/build-jars --- 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 diff -r ad2036bb81c6 -r 4ccb7e635477 src/Pure/library.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