# HG changeset patch
# User wenzelm
# Date 1472936217 -7200
# Node ID f1968429e3396db2b9ab805068ac9c33c691b65b
# Parent  fd6caec306fc5fad1915cb9a1026ff1592adb2f7
minimal support for SQLite databases;

diff -r fd6caec306fc -r f1968429e339 Admin/components/components.sha1
--- a/Admin/components/components.sha1	Fri Sep 02 20:30:54 2016 +0200
+++ b/Admin/components/components.sha1	Sat Sep 03 22:56:57 2016 +0200
@@ -151,6 +151,7 @@
 b447017e81600cc5e30dd61b5d4962f6da01aa80  scala-2.8.1.final.tar.gz
 5659440f6b86db29f0c9c0de7249b7e24a647126  scala-2.9.2.tar.gz
 43b5afbcad575ab6817d2289756ca22fd2ef43a9  spass-3.8ds.tar.gz
+8d20968603f45a2c640081df1ace6a8b0527452a  sqlite-jdbc-3.8.11.2.tar.gz
 1f4a2053cc1f34fa36c4d9d2ac906ad4ebc863fd  sumatra_pdf-2.1.1.tar.gz
 601e08d048d8e50b0729429c8928b667d9b6bde9  sumatra_pdf-2.3.2.tar.gz
 14d46c2eb1a34821703da59d543433f581e91df3  sumatra_pdf-2.4.tar.gz
diff -r fd6caec306fc -r f1968429e339 Admin/components/main
--- a/Admin/components/main	Fri Sep 02 20:30:54 2016 +0200
+++ b/Admin/components/main	Sat Sep 03 22:56:57 2016 +0200
@@ -13,5 +13,6 @@
 polyml-5.6-1
 scala-2.11.8
 spass-3.8ds
+sqlite-jdbc-3.8.11.2
 xz-java-1.2-1
 z3-4.4.0pre
diff -r fd6caec306fc -r f1968429e339 src/Pure/Tools/sqlite.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/sqlite.scala	Sat Sep 03 22:56:57 2016 +0200
@@ -0,0 +1,52 @@
+/*  Title:      Pure/Tools/sqlite.scala
+    Author:     Makarius
+    Options:    :folding=explicit:
+
+Support for SQLite databases.
+*/
+
+package isabelle
+
+
+import java.sql.{Connection, DriverManager}
+
+
+object SQLite
+{
+  /* database connection */
+
+  def open_connection(path: Path): Connection =
+  {
+    val s0 = File.platform_path(path.expand)
+    val s1 = if (Platform.is_windows) s0.replace('\\', '/') else s0
+    DriverManager.getConnection("jdbc:sqlite:" + s1)
+  }
+
+  def with_connection[A](path: Path)(body: Connection => A): A =
+  {
+    val connection = open_connection(path)
+    try { body(connection) } finally { connection.close }
+  }
+
+
+  /* SQL 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 = "`" + s + "`"
+}
diff -r fd6caec306fc -r f1968429e339 src/Pure/build-jars
--- a/src/Pure/build-jars	Fri Sep 02 20:30:54 2016 +0200
+++ b/src/Pure/build-jars	Sat Sep 03 22:56:57 2016 +0200
@@ -116,6 +116,7 @@
   Tools/news.scala
   Tools/print_operation.scala
   Tools/simplifier_trace.scala
+  Tools/sqlite.scala
   Tools/task_statistics.scala
   Tools/update_cartouches.scala
   Tools/update_header.scala