# HG changeset patch
# User wenzelm
# Date 1686842672 -7200
# Node ID c6d4b1a00ad703a230bc32340d821e259b556c2d
# Parent  41a87c4ea765f3f15cf6b7c3ab231afc51001f0e
clarified signature;

diff -r 41a87c4ea765 -r c6d4b1a00ad7 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 {
diff -r 41a87c4ea765 -r c6d4b1a00ad7 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Thu Jun 15 17:03:48 2023 +0200
+++ b/src/Pure/Thy/sessions.scala	Thu Jun 15 17:24:32 2023 +0200
@@ -1517,12 +1517,7 @@
     def open_build_database(): Option[SQL.Database] =
       if (!options.bool("build_database_test")) None
       else if (database_server) Some(open_database_server())
-      else {
-        val db = SQLite.open_database(build_database)
-        try { File.restrict(build_database) }
-        catch { case exn: Throwable => db.close(); throw exn }
-        Some(db)
-      }
+      else Some(SQLite.open_database(build_database, restrict = true))
 
     def try_open_database(
       name: String,
diff -r 41a87c4ea765 -r c6d4b1a00ad7 src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Thu Jun 15 17:03:48 2023 +0200
+++ b/src/Pure/Tools/server.scala	Thu Jun 15 17:24:32 2023 +0200
@@ -397,9 +397,8 @@
     existing_server: Boolean = false,
     log: Logger = No_Logger
   ): (Info, Option[Server]) = {
-    using(SQLite.open_database(Data.database)) { db =>
+    using(SQLite.open_database(Data.database, restrict = true)) { db =>
       db.transaction {
-        File.restrict(Data.database)
         Data.tables.create_lock(db)
         list(db).filterNot(_.active).foreach(server_info =>
           db.execute_statement(Data.table.delete(sql = Data.name.where_equal(server_info.name))))