clarified signature;
authorwenzelm
Thu, 15 Jun 2023 15:04:23 +0200
changeset 78161 4b1b7cbb3e9a
parent 78160 edd1d0bddb24
child 78162 41a87c4ea765
clarified signature;
src/Pure/General/file.scala
src/Pure/General/ssh.scala
src/Pure/ML/ml_process.scala
src/Pure/Thy/sessions.scala
src/Pure/Tools/server.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
--- 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)
--- 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
--- 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)
       }
--- 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))))