# HG changeset patch
# User wenzelm
# Date 1686834263 -7200
# Node ID 4b1b7cbb3e9a92322f86ca4db2dd9ab4e1368414
# Parent  edd1d0bddb246258743481427ecc4ed024a9861a
clarified signature;

diff -r edd1d0bddb24 -r 4b1b7cbb3e9a src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Thu Jun 15 14:45:21 2023 +0200
+++ b/src/Pure/General/file.scala	Thu Jun 15 15:04:23 2023 +0200
@@ -362,6 +362,8 @@
 
   /* permissions */
 
+  def restrict(path: Path): Unit = Isabelle_System.chmod("g-rwx,o-rwx", path)
+
   def is_executable(path: Path): Boolean = {
     if (Platform.is_windows) Isabelle_System.bash("test -x " + bash_path(path)).check.ok
     else path.file.canExecute
diff -r edd1d0bddb24 -r 4b1b7cbb3e9a src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Thu Jun 15 14:45:21 2023 +0200
+++ b/src/Pure/General/ssh.scala	Thu Jun 15 15:04:23 2023 +0200
@@ -241,6 +241,11 @@
       if (cmd.nonEmpty) run_sftp(cmd + " " + sftp_path(path))
     }
 
+    override def restrict(path: Path): Unit =
+      if (!execute("chmod g-rwx,o-rwx " + bash_path(path)).ok) {
+        error("Failed to change permissions of " + quote(remote_path(path)))
+      }
+
     override def set_executable(path: Path, flag: Boolean = false): Unit =
       if (!execute("chmod a" + (if (flag) "+" else "-") + "x " + bash_path(path)).ok) {
         error("Failed to change executable status of " + quote(remote_path(path)))
@@ -402,6 +407,7 @@
     def is_dir(path: Path): Boolean = path.is_dir
     def is_file(path: Path): Boolean = path.is_file
     def delete(path: Path): Unit = path.file.delete
+    def restrict(path: Path): Unit = File.restrict(path)
     def set_executable(path: Path, flag: Boolean = false): Unit =
       File.set_executable(path, flag = flag)
     def make_directory(path: Path): Path = Isabelle_System.make_directory(path)
diff -r edd1d0bddb24 -r 4b1b7cbb3e9a src/Pure/ML/ml_process.scala
--- a/src/Pure/ML/ml_process.scala	Thu Jun 15 14:45:21 2023 +0200
+++ b/src/Pure/ML/ml_process.scala	Thu Jun 15 15:04:23 2023 +0200
@@ -77,13 +77,13 @@
     // options
     val eval_options = if (session_heaps.isEmpty) Nil else List("Options.load_default ()")
     val isabelle_process_options = Isabelle_System.tmp_file("options")
-    Isabelle_System.chmod("600", File.path(isabelle_process_options))
+    File.restrict(File.path(isabelle_process_options))
     File.write(isabelle_process_options, YXML.string_of_body(options.encode))
 
     // session resources
     val eval_init_session = if (session_heaps.isEmpty) Nil else List("Resources.init_session_env ()")
     val init_session = Isabelle_System.tmp_file("init_session")
-    Isabelle_System.chmod("600", File.path(init_session))
+    File.restrict(File.path(init_session))
     File.write(init_session, new Resources(session_background).init_session_yxml)
 
     // process
diff -r edd1d0bddb24 -r 4b1b7cbb3e9a src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Thu Jun 15 14:45:21 2023 +0200
+++ b/src/Pure/Thy/sessions.scala	Thu Jun 15 15:04:23 2023 +0200
@@ -1519,7 +1519,7 @@
       else if (database_server) Some(open_database_server())
       else {
         val db = SQLite.open_database(build_database)
-        try { Isabelle_System.chmod("600", build_database) }
+        try { File.restrict(build_database) }
         catch { case exn: Throwable => db.close(); throw exn }
         Some(db)
       }
diff -r edd1d0bddb24 -r 4b1b7cbb3e9a src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Thu Jun 15 14:45:21 2023 +0200
+++ b/src/Pure/Tools/server.scala	Thu Jun 15 15:04:23 2023 +0200
@@ -399,7 +399,7 @@
   ): (Info, Option[Server]) = {
     using(SQLite.open_database(Data.database)) { db =>
       db.transaction {
-        Isabelle_System.chmod("600", Data.database)
+        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))))