src/Pure/General/sql.scala
changeset 78163 c6d4b1a00ad7
parent 78154 8a7df40375ae
child 78167 1b97502461a3
equal deleted inserted replaced
78162:41a87c4ea765 78163:c6d4b1a00ad7
   492     System.setProperty("org.sqlite.lib.name", lib_name)
   492     System.setProperty("org.sqlite.lib.name", lib_name)
   493 
   493 
   494     Class.forName("org.sqlite.JDBC")
   494     Class.forName("org.sqlite.JDBC")
   495   }
   495   }
   496 
   496 
   497   def open_database(path: Path): Database = {
   497   def open_database(path: Path, restrict: Boolean = false): Database = {
   498     init_jdbc
   498     init_jdbc
   499     val path0 = path.expand
   499     val path0 = path.expand
   500     val s0 = File.platform_path(path0)
   500     val s0 = File.platform_path(path0)
   501     val s1 = if (Platform.is_windows) s0.replace('\\', '/') else s0
   501     val s1 = if (Platform.is_windows) s0.replace('\\', '/') else s0
   502     val connection = DriverManager.getConnection("jdbc:sqlite:" + s1)
   502     val connection = DriverManager.getConnection("jdbc:sqlite:" + s1)
   503     new Database(path0.toString, connection)
   503     val db = new Database(path0.toString, connection)
       
   504 
       
   505     try { if (restrict) File.restrict(path0) }
       
   506     catch { case exn: Throwable => db.close(); throw exn }
       
   507 
       
   508     db
   504   }
   509   }
   505 
   510 
   506   class Database private[SQLite](name: String, val connection: Connection) extends SQL.Database {
   511   class Database private[SQLite](name: String, val connection: Connection) extends SQL.Database {
   507     override def toString: String = name
   512     override def toString: String = name
   508 
   513