# HG changeset patch
# User wenzelm
# Date 1686916890 -7200
# Node ID 5ad1ae8626de658bf5728b516bd28f6cc725594d
# Parent  8fbe3b3d665b1786d20317f0c09c8c23b92d054f
minor performance tuning: avoid external process;

diff -r 8fbe3b3d665b -r 5ad1ae8626de src/Pure/General/file.scala
--- 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