clarified modules;
authorwenzelm
Sun, 24 Mar 2024 18:45:40 +0100
changeset 79977 612f0bb14124
parent 79976 c7e6a508a65b
child 79978 2cc5182cbb08
clarified modules;
src/Pure/System/components.scala
--- a/src/Pure/System/components.scala	Sun Mar 24 17:49:53 2024 +0100
+++ b/src/Pure/System/components.scala	Sun Mar 24 18:45:40 2024 +0100
@@ -89,23 +89,6 @@
     name
   }
 
-  def clean(
-    component_dir: Path,
-    platforms: List[Platform.Family] = Platform.Family.list,
-    ssh: SSH.System = SSH.Local,
-    progress: Progress = new Progress
-  ): Unit = {
-    val purge = platform_purge(platforms)
-    for {
-      name <- ssh.read_dir(component_dir)
-      path = Path.basic(name)
-      if purge(name) && ssh.is_dir(component_dir + path)
-    } {
-      progress.echo("Removing " + (component_dir.base + path))
-      ssh.rm_tree(component_dir + path)
-    }
-  }
-
   def clean_base(
     base_dir: Path,
     platforms: List[Platform.Family] = Platform.Family.list,
@@ -116,7 +99,7 @@
       name <- ssh.read_dir(base_dir)
       dir = base_dir + Path.basic(name)
       if is_component_dir(dir)
-    } clean(dir, platforms = platforms, ssh = ssh, progress = progress)
+    } Directory(dir, ssh = ssh).clean(platforms = platforms, progress = progress)
   }
 
   def resolve(
@@ -148,8 +131,8 @@
     unpack(unpack_dir, archive, ssh = ssh, progress = progress)
 
     if (clean_platforms.isDefined) {
-      clean(unpack_dir + Path.basic(name),
-        platforms = clean_platforms.get, ssh = ssh, progress = progress)
+      Directory(unpack_dir + Path.basic(name), ssh = ssh).
+        clean(platforms = clean_platforms.get, progress = progress)
     }
 
     if (clean_archives) {
@@ -221,6 +204,21 @@
       this
     }
 
+    def clean(
+      platforms: List[Platform.Family] = Platform.Family.list,
+      progress: Progress = new Progress
+    ): Unit = {
+      val purge = platform_purge(platforms)
+      for {
+        name <- ssh.read_dir(path)
+        dir = Path.basic(name)
+        if purge(name) && ssh.is_dir(path + dir)
+      } {
+        progress.echo("Removing " + (path.base + dir))
+        ssh.rm_tree(path + dir)
+      }
+    }
+
     def ok: Boolean =
       ssh.is_file(settings) || ssh.is_file(components) || Sessions.is_session_dir(path, ssh = ssh)