# HG changeset patch
# User wenzelm
# Date 1716558934 -7200
# Node ID b8918a5a669e18481b6584003fdfd39c7acb8da7
# Parent  f895ad113d8082f29e3485254b0b24611c4f73a5
more uniform local/remote operations;

diff -r f895ad113d80 -r b8918a5a669e src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Thu May 23 21:39:40 2024 +0200
+++ b/src/Pure/General/ssh.scala	Fri May 24 15:55:34 2024 +0200
@@ -263,6 +263,9 @@
     override def is_dir(path: Path): Boolean = run_ssh(args = "test -d " + bash_path(path)).ok
     override def is_file(path: Path): Boolean = run_ssh(args = "test -f " + bash_path(path)).ok
 
+    override def eq_file(path1: Path, path2: Path): Boolean =
+      path1 == path2 || execute("test " + bash_path(path1) + " -ef " + bash_path(path2)).ok
+
     override def delete(path: Path): Unit = {
       val cmd = if (is_dir(path)) "rmdir" else if (is_file(path)) "rm" else ""
       if (cmd.nonEmpty) run_sftp(cmd + " " + sftp_path(path))
@@ -286,10 +289,12 @@
     }
 
     override def copy_file(src: Path, dst: Path): Unit = {
-      val direct = if (is_dir(dst)) "/." else ""
-      if (!execute("cp -a " + bash_path(src) + " " + bash_path(dst) + direct).ok) {
-        error("Failed to copy file " + expand_path(src) + " to " +
-          expand_path(dst) + " (ssh " + toString + ")")
+      val target = if (is_dir(dst)) dst + expand_path(src).base else dst
+      if (!eq_file(src, target)) {
+        if (!execute("cp -a " + bash_path(src) + " " + bash_path(target)).ok) {
+          error("Failed to copy file " +
+            absolute_path(src) + " to " + absolute_path(target) + " (ssh " + toString + ")")
+        }
       }
     }
 
@@ -479,6 +484,7 @@
     def bash_path(path: Path): String = File.bash_path(path)
     def is_dir(path: Path): Boolean = path.is_dir
     def is_file(path: Path): Boolean = path.is_file
+    def eq_file(path1: Path, path2: Path): Boolean = File.eq(path1, path2)
     def delete(path: Path): Unit = path.file.delete
     def restrict(path: Path): Unit = File.restrict(path)
     def set_executable(path: Path, reset: Boolean = false): Unit =
diff -r f895ad113d80 -r b8918a5a669e src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Thu May 23 21:39:40 2024 +0200
+++ b/src/Pure/System/isabelle_system.scala	Fri May 24 15:55:34 2024 +0200
@@ -223,7 +223,7 @@
       catch {
         case ERROR(msg) =>
           cat_error("Failed to copy file " +
-            File.path(src).absolute + " to " + File.path(dst).absolute, msg)
+            File.path(src).absolute + " to " + File.path(target).absolute, msg)
       }
     }
   }