--- 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))))