# HG changeset patch
# User wenzelm
# Date 1573727702 -3600
# Node ID 6cfec802983136502d4b080efd3ff6cce2ecf1b0
# Parent  153ed199c0d4095ef1d3271fd9c1b4f7623e2640
clarified signature;

diff -r 153ed199c0d4 -r 6cfec8029831 src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Wed Nov 13 20:21:05 2019 +0100
+++ b/src/Pure/General/file.scala	Thu Nov 14 11:35:02 2019 +0100
@@ -351,8 +351,8 @@
 
   def set_executable(path: Path, flag: Boolean)
   {
-    if (Platform.is_windows && flag) Isabelle_System.bash("chmod a+x " + bash_path(path)).check
-    else if (Platform.is_windows) Isabelle_System.bash("chmod a-x " + bash_path(path)).check
+    if (Platform.is_windows && flag) Isabelle_System.chmod("a+x", path)
+    else if (Platform.is_windows) Isabelle_System.chmod("a-x", path)
     else path.file.setExecutable(flag, false)
   }
 }
diff -r 153ed199c0d4 -r 6cfec8029831 src/Pure/ML/ml_process.scala
--- a/src/Pure/ML/ml_process.scala	Wed Nov 13 20:21:05 2019 +0100
+++ b/src/Pure/ML/ml_process.scala	Thu Nov 14 11:35:02 2019 +0100
@@ -75,7 +75,7 @@
 
     // options
     val isabelle_process_options = Isabelle_System.tmp_file("options")
-    Isabelle_System.bash("chmod 600 " + File.bash_path(File.path(isabelle_process_options))).check
+    Isabelle_System.chmod("600", File.path(isabelle_process_options))
     File.write(isabelle_process_options, YXML.string_of_body(options.encode))
     val env_options = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options))
     val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()")
diff -r 153ed199c0d4 -r 6cfec8029831 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Wed Nov 13 20:21:05 2019 +0100
+++ b/src/Pure/System/isabelle_system.scala	Thu Nov 14 11:35:02 2019 +0100
@@ -149,6 +149,15 @@
 
   /** file-system operations **/
 
+  /* permissions */
+
+  def chmod(arg: String, path: Path): Unit =
+    bash("chmod " + Bash.string(arg) + " -- " + File.bash_path(path)).check
+
+  def chown(arg: String, path: Path): Unit =
+    bash("chown " + Bash.string(arg) + " -- " + File.bash_path(path)).check
+
+
   /* directories */
 
   def mkdirs(path: Path): Unit =
diff -r 153ed199c0d4 -r 6cfec8029831 src/Pure/System/linux.scala
--- a/src/Pure/System/linux.scala	Wed Nov 13 20:21:05 2019 +0100
+++ b/src/Pure/System/linux.scala	Thu Nov 14 11:35:02 2019 +0100
@@ -133,7 +133,7 @@
 
     val service_file = Path.explode("/lib/systemd/system") + Path.basic(name).ext("service")
     File.write(service_file, spec)
-    Isabelle_System.bash("chmod 0644 " + File.bash_path(service_file)).check
+    Isabelle_System.chmod("0644", service_file)
 
     service_enable(name)
     service_restart(name)
diff -r 153ed199c0d4 -r 6cfec8029831 src/Pure/Thy/present.scala
--- a/src/Pure/Thy/present.scala	Wed Nov 13 20:21:05 2019 +0100
+++ b/src/Pure/Thy/present.scala	Thu Nov 14 11:35:02 2019 +0100
@@ -92,7 +92,7 @@
 
       val session_graph = session_prefix + Path.basic("session_graph.pdf")
       File.copy(graph_file, session_graph.file)
-      Isabelle_System.bash("chmod a+r " + File.bash_path(session_graph))
+      Isabelle_System.chmod("a+r", session_graph)
 
       HTML.write_isabelle_css(session_prefix)
 
diff -r 153ed199c0d4 -r 6cfec8029831 src/Pure/Tools/phabricator.scala
--- a/src/Pure/Tools/phabricator.scala	Wed Nov 13 20:21:05 2019 +0100
+++ b/src/Pure/Tools/phabricator.scala	Thu Nov 14 11:35:02 2019 +0100
@@ -230,12 +230,9 @@
       error("Failed to create local repository directory " + repo_path)
     }
 
-    Isabelle_System.bash(cwd = repo_path.file,
-      script = """
-        set -e
-        chown -R """ + Bash.string(daemon_user) + ":" + Bash.string(daemon_user) + """ .
-        chmod 755 .
-      """).check
+    Isabelle_System.chown(
+      "-R " + Bash.string(daemon_user) + ":" + Bash.string(daemon_user), repo_path)
+    Isabelle_System.chmod("755", repo_path)
 
     config.execute("config set repository.default-local-path " + File.bash_path(repo_path))
 
@@ -245,7 +242,7 @@
       www_user + " ALL=(" + daemon_user + ") SETENV: NOPASSWD: /usr/bin/git, /usr/bin/hg, /usr/bin/ssh, /usr/bin/id\n" +
       name + " ALL=(" + daemon_user + ") SETENV: NOPASSWD: /usr/bin/git, /usr/bin/git-upload-pack, /usr/bin/git-receive-pack, /usr/bin/hg, /usr/bin/svnserve, /usr/bin/ssh, /usr/bin/id\n")
 
-    Isabelle_System.bash("chmod 0440 " + File.bash_path(sudoers_file)).check
+    Isabelle_System.chmod("0440", sudoers_file)
 
     config.execute("config set diffusion.ssh-user " + Bash.string(config.name))
 
@@ -455,7 +452,7 @@
     if (config_file.isEmpty) {
       if (!default_config_file.is_file) {
         File.write(default_config_file, mailers_template)
-        Isabelle_System.bash("chmod 600 " + File.bash_path(default_config_file)).check
+        Isabelle_System.chmod("600", default_config_file)
       }
       if (File.read(default_config_file) == mailers_template) {
         progress.echo(
@@ -598,8 +595,8 @@
   exit 1
 } < /etc/isabelle-phabricator.conf
 """)
-    Isabelle_System.bash("chmod 755 " + File.bash_path(ssh_command)).check
-    Isabelle_System.bash("chown root:root " + File.bash_path(ssh_command)).check
+    Isabelle_System.chmod("755", ssh_command)
+    Isabelle_System.chown("root:root", ssh_command)
 
     File.write(sshd_conf_server,
 """# OpenBSD Secure Shell server for Isabelle/Phabricator
diff -r 153ed199c0d4 -r 6cfec8029831 src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Wed Nov 13 20:21:05 2019 +0100
+++ b/src/Pure/Tools/server.scala	Thu Nov 14 11:35:02 2019 +0100
@@ -404,7 +404,7 @@
     using(SQLite.open_database(Data.database))(db =>
       {
         db.transaction {
-          Isabelle_System.bash("chmod 600 " + File.bash_path(Data.database)).check
+          Isabelle_System.chmod("600", Data.database)
           db.create_table(Data.table)
           list(db).filterNot(_.active).foreach(server_info =>
             db.using_statement(Data.table.delete(Data.name.where_equal(server_info.name)))(