# HG changeset patch
# User wenzelm
# Date 1689068243 -7200
# Node ID 3b0f8f1010f239735ce53828dce8e835bf2e3207
# Parent  ba3729a9d29da92ff5cd26bfb21146d94f483146
clarified signature, with subtle change of semantics (amending 8b5a2e4b16d4);

diff -r ba3729a9d29d -r 3b0f8f1010f2 NEWS
--- a/NEWS	Mon Jul 10 22:44:28 2023 +0200
+++ b/NEWS	Tue Jul 11 11:37:23 2023 +0200
@@ -456,6 +456,9 @@
 via Compress.Options and Compress.Cache. Bytes.uncompress automatically
 detects the compression scheme.
 
+* File.set_executable in Isabelle/Scala has changed its mandatory "flag"
+to optional "reset", which opposite polarity. INCOMPATIBILITY.
+
 
 
 New in Isabelle2022 (October 2022)
diff -r ba3729a9d29d -r 3b0f8f1010f2 src/Pure/Admin/component_zstd.scala
--- a/src/Pure/Admin/component_zstd.scala	Mon Jul 10 22:44:28 2023 +0200
+++ b/src/Pure/Admin/component_zstd.scala	Tue Jul 11 11:37:23 2023 +0200
@@ -15,7 +15,7 @@
       val source = jar_dir + Path.explode(template.replace("{V}", version))
       val target = Isabelle_System.make_directory(component_dir + Path.basic(name))
       Isabelle_System.copy_file(source, target)
-      if (exe) File.set_executable(target + source.base, true)
+      if (exe) File.set_executable(target + source.base)
     }
   }
 
diff -r ba3729a9d29d -r 3b0f8f1010f2 src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Mon Jul 10 22:44:28 2023 +0200
+++ b/src/Pure/General/file.scala	Tue Jul 11 11:37:23 2023 +0200
@@ -388,10 +388,9 @@
     else path.file.canExecute
   }
 
-  def set_executable(path: Path, flag: Boolean = false): Unit = {
-    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)
+  def set_executable(path: Path, reset: Boolean = false): Unit = {
+    if (Platform.is_windows) Isabelle_System.chmod(if (reset) "a-x" else "a+x", path)
+    else path.file.setExecutable(!reset, false)
   }
 
 
diff -r ba3729a9d29d -r 3b0f8f1010f2 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Mon Jul 10 22:44:28 2023 +0200
+++ b/src/Pure/General/ssh.scala	Tue Jul 11 11:37:23 2023 +0200
@@ -246,8 +246,8 @@
         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) {
+    override def set_executable(path: Path, reset: Boolean = false): Unit =
+      if (!execute("chmod a" + (if (reset) "-" else "+") + "x " + bash_path(path)).ok) {
         error("Failed to change executable status of " + quote(remote_path(path)))
       }
 
@@ -408,8 +408,8 @@
     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 set_executable(path: Path, reset: Boolean = false): Unit =
+      File.set_executable(path, reset = reset)
     def make_directory(path: Path): Path = Isabelle_System.make_directory(path)
     def rm_tree(dir: Path): Unit = Isabelle_System.rm_tree(dir)
     def with_tmp_dir[A](body: Path => A): A = Isabelle_System.with_tmp_dir("tmp")(body)
diff -r ba3729a9d29d -r 3b0f8f1010f2 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Mon Jul 10 22:44:28 2023 +0200
+++ b/src/Pure/Thy/export.scala	Tue Jul 11 11:37:23 2023 +0200
@@ -548,7 +548,7 @@
           Isabelle_System.make_directory(path.dir)
           val bytes = entry.bytes
           if (!path.is_file || Bytes.read(path) != bytes) Bytes.write(path, bytes)
-          File.set_executable(path, flag = entry.executable)
+          File.set_executable(path, reset = !entry.executable)
         }
       }
     }