clarified modules;
tuned signature;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/sql.scala	Sun Sep 04 15:44:20 2016 +0200
@@ -0,0 +1,32 @@
+/*  Title:      Pure/Tools/sql.scala
+    Author:     Makarius
+
+Support for SQL.
+*/
+
+package isabelle
+
+
+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 = "`" + s + "`"
+}

--- a/src/Pure/Tools/sqlite.scala	Sat Sep 03 23:25:02 2016 +0200
+++ b/src/Pure/Tools/sqlite.scala	Sun Sep 04 15:44:20 2016 +0200
@@ -14,38 +14,25 @@
 {
   /* database connection */
 
-  def open_connection(path: Path): Connection =
+  class Database private [SQLite](path: Path, val connection: Connection)
   {
-    val s0 = File.platform_path(path.expand)
-    val s1 = if (Platform.is_windows) s0.replace('\\', '/') else s0
-    DriverManager.getConnection("jdbc:sqlite:" + s1)
-  }
+    override def toString: String = path.toString
 
-  def with_connection[A](path: Path)(body: Connection => A): A =
-  {
-    val connection = open_connection(path)
-    try { body(connection) } finally { connection.close }
+    def close { connection.close }
   }
 
-
-  /* SQL syntax */
+  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 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 + "`"
+  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	Sat Sep 03 23:25:02 2016 +0200
+++ b/src/Pure/build-jars	Sun Sep 04 15:44:20 2016 +0200
@@ -116,6 +116,7 @@
   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