src/Pure/General/sql.scala

--- a/src/Pure/General/sql.scala	Thu Jun 15 17:03:48 2023 +0200
+++ b/src/Pure/General/sql.scala	Thu Jun 15 17:24:32 2023 +0200
@@ -494,13 +494,18 @@
     Class.forName("org.sqlite.JDBC")
   }
 
-  def open_database(path: Path): Database = {
+  def open_database(path: Path, restrict: Boolean = false): Database = {
     init_jdbc
     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.toString, connection)
+    val db = new Database(path0.toString, connection)
+
+    try { if (restrict) File.restrict(path0) }
+    catch { case exn: Throwable => db.close(); throw exn }
+
+    db
   }
 
   class Database private[SQLite](name: String, val connection: Connection) extends SQL.Database {