--- a/src/Pure/General/file.scala Thu Jun 15 22:09:56 2023 +0200
+++ b/src/Pure/General/file.scala Fri Jun 16 14:01:30 2023 +0200
@@ -12,7 +12,7 @@
InputStreamReader, File => JFile, IOException}
import java.nio.file.{StandardOpenOption, Path => JPath, Files, SimpleFileVisitor,
FileVisitOption, FileVisitResult}
-import java.nio.file.attribute.BasicFileAttributes
+import java.nio.file.attribute.{BasicFileAttributes, PosixFilePermission}
import java.net.{URI, URL, MalformedURLException}
import java.util.zip.{GZIPInputStream, GZIPOutputStream}
import java.util.EnumSet
@@ -362,7 +362,26 @@
/* permissions */
- def restrict(path: Path): Unit = Isabelle_System.chmod("g-rwx,o-rwx", path)
+ private val restrict_perms: List[PosixFilePermission] =
+ List(
+ PosixFilePermission.GROUP_READ,
+ PosixFilePermission.GROUP_WRITE,
+ PosixFilePermission.GROUP_EXECUTE,
+ PosixFilePermission.OTHERS_READ,
+ PosixFilePermission.OTHERS_WRITE,
+ PosixFilePermission.OTHERS_EXECUTE)
+
+ def restrict(path: Path): Unit =
+ if (Platform.is_windows) Isabelle_System.chmod("g-rwx,o-rwx", path)
+ else {
+ val perms = Files.getPosixFilePermissions(path.java_path)
+ var perms_changed = false
+ for (p <- restrict_perms if perms.contains(p)) {
+ perms.remove(p)
+ perms_changed = true
+ }
+ if (perms_changed) Files.setPosixFilePermissions(path.java_path, perms)
+ }
def is_executable(path: Path): Boolean = {
if (Platform.is_windows) Isabelle_System.bash("test -x " + bash_path(path)).check.ok