# HG changeset patch # User wenzelm # Date 1711302340 -3600 # Node ID 612f0bb14124d927d2b4486f9bc32ef6dbd9600f # Parent c7e6a508a65b88aa1c3aa19e2623d4656d5346f3 clarified modules; diff -r c7e6a508a65b -r 612f0bb14124 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)