clarified modules;
authorwenzelm
Sun Sep 04 15:44:20 2016 +0200 (2016-09-04)
changeset 63778e06e899b78d0
parent 63777 fc030773ec90
child 63779 9da65bc75610
clarified modules;
tuned signature;
src/Pure/Tools/sql.scala
src/Pure/Tools/sqlite.scala
src/Pure/build-jars
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Tools/sql.scala	Sun Sep 04 15:44:20 2016 +0200
     1.3 @@ -0,0 +1,32 @@
     1.4 +/*  Title:      Pure/Tools/sql.scala
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Support for SQL.
     1.8 +*/
     1.9 +
    1.10 +package isabelle
    1.11 +
    1.12 +
    1.13 +object SQL
    1.14 +{
    1.15 +  /* concrete syntax */
    1.16 +
    1.17 +  def quote_char(c: Char): String =
    1.18 +    c match {
    1.19 +      case '\u0000' => "\\0"
    1.20 +      case '\'' => "\\'"
    1.21 +      case '\"' => "\\\""
    1.22 +      case '\b' => "\\b"
    1.23 +      case '\n' => "\\n"
    1.24 +      case '\r' => "\\r"
    1.25 +      case '\t' => "\\t"
    1.26 +      case '\u001a' => "\\Z"
    1.27 +      case '\\' => "\\\\"
    1.28 +      case _ => c.toString
    1.29 +    }
    1.30 +
    1.31 +  def quote_string(s: String): String =
    1.32 +    quote(s.map(quote_char(_)).mkString)
    1.33 +
    1.34 +  def quote_ident(s: String): String = "`" + s + "`"
    1.35 +}
     2.1 --- a/src/Pure/Tools/sqlite.scala	Sat Sep 03 23:25:02 2016 +0200
     2.2 +++ b/src/Pure/Tools/sqlite.scala	Sun Sep 04 15:44:20 2016 +0200
     2.3 @@ -14,38 +14,25 @@
     2.4  {
     2.5    /* database connection */
     2.6  
     2.7 -  def open_connection(path: Path): Connection =
     2.8 +  class Database private [SQLite](path: Path, val connection: Connection)
     2.9    {
    2.10 -    val s0 = File.platform_path(path.expand)
    2.11 -    val s1 = if (Platform.is_windows) s0.replace('\\', '/') else s0
    2.12 -    DriverManager.getConnection("jdbc:sqlite:" + s1)
    2.13 -  }
    2.14 +    override def toString: String = path.toString
    2.15  
    2.16 -  def with_connection[A](path: Path)(body: Connection => A): A =
    2.17 -  {
    2.18 -    val connection = open_connection(path)
    2.19 -    try { body(connection) } finally { connection.close }
    2.20 +    def close { connection.close }
    2.21    }
    2.22  
    2.23 -
    2.24 -  /* SQL syntax */
    2.25 +  def open_database(path: Path): Database =
    2.26 +  {
    2.27 +    val path0 = path.expand
    2.28 +    val s0 = File.platform_path(path0)
    2.29 +    val s1 = if (Platform.is_windows) s0.replace('\\', '/') else s0
    2.30 +    val connection = DriverManager.getConnection("jdbc:sqlite:" + s1)
    2.31 +    new Database(path0, connection)
    2.32 +  }
    2.33  
    2.34 -  def quote_char(c: Char): String =
    2.35 -    c match {
    2.36 -      case '\u0000' => "\\0"
    2.37 -      case '\'' => "\\'"
    2.38 -      case '\"' => "\\\""
    2.39 -      case '\b' => "\\b"
    2.40 -      case '\n' => "\\n"
    2.41 -      case '\r' => "\\r"
    2.42 -      case '\t' => "\\t"
    2.43 -      case '\u001a' => "\\Z"
    2.44 -      case '\\' => "\\\\"
    2.45 -      case _ => c.toString
    2.46 -    }
    2.47 -
    2.48 -  def quote_string(s: String): String =
    2.49 -    quote(s.map(quote_char(_)).mkString)
    2.50 -
    2.51 -  def quote_ident(s: String): String = "`" + s + "`"
    2.52 +  def with_database[A](path: Path)(body: Database => A): A =
    2.53 +  {
    2.54 +    val db = open_database(path)
    2.55 +    try { body(db) } finally { db.close }
    2.56 +  }
    2.57  }
     3.1 --- a/src/Pure/build-jars	Sat Sep 03 23:25:02 2016 +0200
     3.2 +++ b/src/Pure/build-jars	Sun Sep 04 15:44:20 2016 +0200
     3.3 @@ -116,6 +116,7 @@
     3.4    Tools/news.scala
     3.5    Tools/print_operation.scala
     3.6    Tools/simplifier_trace.scala
     3.7 +  Tools/sql.scala
     3.8    Tools/sqlite.scala
     3.9    Tools/task_statistics.scala
    3.10    Tools/update_cartouches.scala