clarified signature;
authorwenzelm
Fri, 24 May 2024 19:15:51 +0200
changeset 80192 36e6ba1527f0
parent 80191 c934f0e51f1c
child 80193 ed8a3f4e3de7
clarified signature;
src/Pure/General/rsync.scala
src/Pure/General/url.scala
src/Pure/System/isabelle_system.scala
--- a/src/Pure/General/rsync.scala	Fri May 24 17:31:49 2024 +0200
+++ b/src/Pure/General/rsync.scala	Fri May 24 19:15:51 2024 +0200
@@ -40,10 +40,8 @@
         (if (stats) " --stats" else "")
     }
 
-    def target(path: Path, direct: Boolean = false): String = {
-      val s = ssh.rsync_path(path)
-      if (direct) Url.direct_path(s) else s
-    }
+    def target(path: Path, direct: Boolean = false): String =
+      Url.dir_path(ssh.rsync_path(path), direct = direct)
   }
 
   def exec(
--- a/src/Pure/General/url.scala	Fri May 24 17:31:49 2024 +0200
+++ b/src/Pure/General/url.scala	Fri May 24 19:15:51 2024 +0200
@@ -145,6 +145,9 @@
     else prefix + "/" + suffix
 
   def direct_path(prefix: String): String = append_path(prefix, ".")
+
+  def dir_path(prefix: String, direct: Boolean = false): String =
+    if (direct) direct_path(prefix) else prefix
 }
 
 final class Url private(val uri: URI) {
--- a/src/Pure/System/isabelle_system.scala	Fri May 24 17:31:49 2024 +0200
+++ b/src/Pure/System/isabelle_system.scala	Fri May 24 19:15:51 2024 +0200
@@ -181,10 +181,8 @@
     else make_directory(path)
 
   def copy_dir(dir1: Path, dir2: Path, direct: Boolean = false): Unit = {
-    def make_path(dir: Path): String = {
-      val s = File.standard_path(dir.absolute)
-      if (direct) Url.direct_path(s) else s
-    }
+    def make_path(dir: Path): String =
+      Url.dir_path(File.standard_path(dir.absolute), direct = direct)
     val p1 = make_path(dir1)
     val p2 = make_path(dir2)
     make_directory(if (direct) dir2.absolute else dir2.absolute.dir)