src/Pure/General/sql.scala
changeset 65021 da8ae577d171
parent 65020 a4fcaeadc825
child 65022 cda3d36aceb2
equal deleted inserted replaced
65020:a4fcaeadc825 65021:da8ae577d171
     4 Support for SQL databases: SQLite and PostgreSQL.
     4 Support for SQL databases: SQLite and PostgreSQL.
     5 */
     5 */
     6 
     6 
     7 package isabelle
     7 package isabelle
     8 
     8 
     9 
     9 import java.time.OffsetDateTime
    10 import java.sql.{DriverManager, Connection, PreparedStatement, ResultSet, Timestamp}
    10 import java.sql.{DriverManager, Connection, PreparedStatement, ResultSet}
    11 
    11 
    12 
    12 
    13 object SQL
    13 object SQL
    14 {
    14 {
    15   /** SQL language **/
    15   /** SQL language **/
   205     def set_double(stmt: PreparedStatement, i: Int, x: Double) { stmt.setDouble(i, x) }
   205     def set_double(stmt: PreparedStatement, i: Int, x: Double) { stmt.setDouble(i, x) }
   206     def set_string(stmt: PreparedStatement, i: Int, x: String) { stmt.setString(i, x) }
   206     def set_string(stmt: PreparedStatement, i: Int, x: String) { stmt.setString(i, x) }
   207     def set_bytes(stmt: PreparedStatement, i: Int, bytes: Bytes)
   207     def set_bytes(stmt: PreparedStatement, i: Int, bytes: Bytes)
   208     { stmt.setBinaryStream(i, bytes.stream(), bytes.length) }
   208     { stmt.setBinaryStream(i, bytes.stream(), bytes.length) }
   209     def set_date(stmt: PreparedStatement, i: Int, date: Date)
   209     def set_date(stmt: PreparedStatement, i: Int, date: Date)
   210     { stmt.setTimestamp(i, date.timestamp) }
       
   211 
       
   212 
   210 
   213     /* output */
   211     /* output */
   214 
   212 
   215     def bool(rs: ResultSet, name: String): Boolean = rs.getBoolean(name)
   213     def bool(rs: ResultSet, name: String): Boolean = rs.getBoolean(name)
   216     def int(rs: ResultSet, name: String): Int = rs.getInt(name)
   214     def int(rs: ResultSet, name: String): Int = rs.getInt(name)
   224     def bytes(rs: ResultSet, name: String): Bytes =
   222     def bytes(rs: ResultSet, name: String): Bytes =
   225     {
   223     {
   226       val bs = rs.getBytes(name)
   224       val bs = rs.getBytes(name)
   227       if (bs == null) Bytes.empty else Bytes(bs)
   225       if (bs == null) Bytes.empty else Bytes(bs)
   228     }
   226     }
   229     def date(rs: ResultSet, name: String): Date =
   227     def date(rs: ResultSet, name: String): Date
   230       Date.instant(rs.getTimestamp(name).toInstant)
       
   231 
   228 
   232     def get[A](rs: ResultSet, name: String, f: (ResultSet, String) => A): Option[A] =
   229     def get[A](rs: ResultSet, name: String, f: (ResultSet, String) => A): Option[A] =
   233     {
   230     {
   234       val x = f(rs, name)
   231       val x = f(rs, name)
   235       if (rs.wasNull) None else Some(x)
   232       if (rs.wasNull) None else Some(x)
   260 
   257 
   261 /** SQLite **/
   258 /** SQLite **/
   262 
   259 
   263 object SQLite
   260 object SQLite
   264 {
   261 {
       
   262   // see https://www.sqlite.org/lang_datefunc.html
       
   263   val date_format: Date.Format = Date.Format("uuuu-MM-dd HH:mm:ss.SSS x")
       
   264 
   265   def open_database(path: Path): Database =
   265   def open_database(path: Path): Database =
   266   {
   266   {
   267     val path0 = path.expand
   267     val path0 = path.expand
   268     val s0 = File.platform_path(path0)
   268     val s0 = File.platform_path(path0)
   269     val s1 = if (Platform.is_windows) s0.replace('\\', '/') else s0
   269     val s1 = if (Platform.is_windows) s0.replace('\\', '/') else s0
   274   class Database private[SQLite](name: String, val connection: Connection) extends SQL.Database
   274   class Database private[SQLite](name: String, val connection: Connection) extends SQL.Database
   275   {
   275   {
   276     override def toString: String = name
   276     override def toString: String = name
   277 
   277 
   278     def sql_type(T: SQL.Type.Value): String = SQL.sql_type_sqlite(T)
   278     def sql_type(T: SQL.Type.Value): String = SQL.sql_type_sqlite(T)
       
   279 
       
   280     def set_date(stmt: PreparedStatement, i: Int, date: Date): Unit =
       
   281       set_string(stmt, i, date_format(date))
       
   282     def date(rs: ResultSet, name: String): Date =
       
   283       date_format.parse(string(rs, name))
   279 
   284 
   280     def rebuild { using(statement("VACUUM"))(_.execute()) }
   285     def rebuild { using(statement("VACUUM"))(_.execute()) }
   281   }
   286   }
   282 }
   287 }
   283 
   288 
   329   {
   334   {
   330     override def toString: String = name
   335     override def toString: String = name
   331 
   336 
   332     def sql_type(T: SQL.Type.Value): String = SQL.sql_type_postgresql(T)
   337     def sql_type(T: SQL.Type.Value): String = SQL.sql_type_postgresql(T)
   333 
   338 
       
   339     // see https://jdbc.postgresql.org/documentation/head/8-date-time.html
       
   340     def set_date(stmt: PreparedStatement, i: Int, date: Date): Unit =
       
   341       stmt.setObject(i, OffsetDateTime.from(date.to_utc.rep))
       
   342     def date(rs: ResultSet, name: String): Date =
       
   343       Date.instant(rs.getObject(name, classOf[OffsetDateTime]).toInstant)
       
   344 
   334     override def close() { super.close; port_forwarding.foreach(_.close) }
   345     override def close() { super.close; port_forwarding.foreach(_.close) }
   335   }
   346   }
   336 }
   347 }