src/Pure/General/sql.scala
changeset 65292 e3bd1e7ddd23
parent 65280 ef37f5236794
child 65319 64da14387b2c
     1.1 --- a/src/Pure/General/sql.scala	Fri Mar 17 20:21:01 2017 +0100
     1.2 +++ b/src/Pure/General/sql.scala	Fri Mar 17 20:33:27 2017 +0100
     1.3 @@ -264,8 +264,11 @@
     1.4    // see https://www.sqlite.org/lang_datefunc.html
     1.5    val date_format: Date.Format = Date.Format("uuuu-MM-dd HH:mm:ss.SSS x")
     1.6  
     1.7 +  lazy val init_jdbc: Unit = Class.forName("org.sqlite.JDBC")
     1.8 +
     1.9    def open_database(path: Path): Database =
    1.10    {
    1.11 +    init_jdbc
    1.12      val path0 = path.expand
    1.13      val s0 = File.platform_path(path0)
    1.14      val s1 = if (Platform.is_windows) s0.replace('\\', '/') else s0
    1.15 @@ -296,6 +299,8 @@
    1.16  {
    1.17    val default_port = 5432
    1.18  
    1.19 +  lazy val init_jdbc: Unit = Class.forName("org.postgresql.Driver")
    1.20 +
    1.21    def open_database(
    1.22      user: String,
    1.23      password: String,
    1.24 @@ -304,6 +309,8 @@
    1.25      port: Int = default_port,
    1.26      ssh: Option[SSH.Session] = None): Database =
    1.27    {
    1.28 +    init_jdbc
    1.29 +
    1.30      require(user != "")
    1.31  
    1.32      val db_host = if (host != "") host else "localhost"