minimal support for SQLite databases;
authorwenzelm
Sat Sep 03 22:56:57 2016 +0200 (2016-09-03)
changeset 63776f1968429e339
parent 63775 fd6caec306fc
child 63777 fc030773ec90
minimal support for SQLite databases;
Admin/components/components.sha1
Admin/components/main
src/Pure/Tools/sqlite.scala
src/Pure/build-jars
     1.1 --- a/Admin/components/components.sha1	Fri Sep 02 20:30:54 2016 +0200
     1.2 +++ b/Admin/components/components.sha1	Sat Sep 03 22:56:57 2016 +0200
     1.3 @@ -151,6 +151,7 @@
     1.4  b447017e81600cc5e30dd61b5d4962f6da01aa80  scala-2.8.1.final.tar.gz
     1.5  5659440f6b86db29f0c9c0de7249b7e24a647126  scala-2.9.2.tar.gz
     1.6  43b5afbcad575ab6817d2289756ca22fd2ef43a9  spass-3.8ds.tar.gz
     1.7 +8d20968603f45a2c640081df1ace6a8b0527452a  sqlite-jdbc-3.8.11.2.tar.gz
     1.8  1f4a2053cc1f34fa36c4d9d2ac906ad4ebc863fd  sumatra_pdf-2.1.1.tar.gz
     1.9  601e08d048d8e50b0729429c8928b667d9b6bde9  sumatra_pdf-2.3.2.tar.gz
    1.10  14d46c2eb1a34821703da59d543433f581e91df3  sumatra_pdf-2.4.tar.gz
     2.1 --- a/Admin/components/main	Fri Sep 02 20:30:54 2016 +0200
     2.2 +++ b/Admin/components/main	Sat Sep 03 22:56:57 2016 +0200
     2.3 @@ -13,5 +13,6 @@
     2.4  polyml-5.6-1
     2.5  scala-2.11.8
     2.6  spass-3.8ds
     2.7 +sqlite-jdbc-3.8.11.2
     2.8  xz-java-1.2-1
     2.9  z3-4.4.0pre
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/Tools/sqlite.scala	Sat Sep 03 22:56:57 2016 +0200
     3.3 @@ -0,0 +1,52 @@
     3.4 +/*  Title:      Pure/Tools/sqlite.scala
     3.5 +    Author:     Makarius
     3.6 +    Options:    :folding=explicit:
     3.7 +
     3.8 +Support for SQLite databases.
     3.9 +*/
    3.10 +
    3.11 +package isabelle
    3.12 +
    3.13 +
    3.14 +import java.sql.{Connection, DriverManager}
    3.15 +
    3.16 +
    3.17 +object SQLite
    3.18 +{
    3.19 +  /* database connection */
    3.20 +
    3.21 +  def open_connection(path: Path): Connection =
    3.22 +  {
    3.23 +    val s0 = File.platform_path(path.expand)
    3.24 +    val s1 = if (Platform.is_windows) s0.replace('\\', '/') else s0
    3.25 +    DriverManager.getConnection("jdbc:sqlite:" + s1)
    3.26 +  }
    3.27 +
    3.28 +  def with_connection[A](path: Path)(body: Connection => A): A =
    3.29 +  {
    3.30 +    val connection = open_connection(path)
    3.31 +    try { body(connection) } finally { connection.close }
    3.32 +  }
    3.33 +
    3.34 +
    3.35 +  /* SQL syntax */
    3.36 +
    3.37 +  def quote_char(c: Char): String =
    3.38 +    c match {
    3.39 +      case '\u0000' => "\\0"
    3.40 +      case '\'' => "\\'"
    3.41 +      case '\"' => "\\\""
    3.42 +      case '\b' => "\\b"
    3.43 +      case '\n' => "\\n"
    3.44 +      case '\r' => "\\r"
    3.45 +      case '\t' => "\\t"
    3.46 +      case '\u001a' => "\\Z"
    3.47 +      case '\\' => "\\\\"
    3.48 +      case _ => c.toString
    3.49 +    }
    3.50 +
    3.51 +  def quote_string(s: String): String =
    3.52 +    quote(s.map(quote_char(_)).mkString)
    3.53 +
    3.54 +  def quote_ident(s: String): String = "`" + s + "`"
    3.55 +}
     4.1 --- a/src/Pure/build-jars	Fri Sep 02 20:30:54 2016 +0200
     4.2 +++ b/src/Pure/build-jars	Sat Sep 03 22:56:57 2016 +0200
     4.3 @@ -116,6 +116,7 @@
     4.4    Tools/news.scala
     4.5    Tools/print_operation.scala
     4.6    Tools/simplifier_trace.scala
     4.7 +  Tools/sqlite.scala
     4.8    Tools/task_statistics.scala
     4.9    Tools/update_cartouches.scala
    4.10    Tools/update_header.scala