# HG changeset patch # User wenzelm # Date 1680179131 -7200 # Node ID 34178d26a360be58a4606f9b263c8b602ca6421a # Parent f513f754c0260a57713e62331604654d819b50c5 more SSH operations; diff -r f513f754c026 -r 34178d26a360 src/Pure/General/ssh.scala --- a/src/Pure/General/ssh.scala Thu Mar 30 12:56:29 2023 +0200 +++ b/src/Pure/General/ssh.scala Thu Mar 30 14:25:31 2023 +0200 @@ -408,6 +408,10 @@ env = if (settings) Isabelle_System.settings() else null, strict = strict) + def new_directory(path: Path): Path = + if (is_dir(path)) error("Directory already exists: " + absolute_path(path)) + else make_directory(path) + def download_file(url_name: String, file: Path, progress: Progress = new Progress): Unit = Isabelle_System.download_file(url_name, file, progress = progress) diff -r f513f754c026 -r 34178d26a360 src/Pure/System/components.scala --- a/src/Pure/System/components.scala Thu Mar 30 12:56:29 2023 +0200 +++ b/src/Pure/System/components.scala Thu Mar 30 14:25:31 2023 +0200 @@ -171,10 +171,11 @@ /* component directory content */ object Directory { - def apply(path: Path): Directory = new Directory(path.absolute) + def apply(path: Path, ssh: SSH.System = SSH.Local): Directory = + new Directory(ssh.absolute_path(path), ssh) } - class Directory private(val path: Path) { + class Directory private(val path: Path, val ssh: SSH.System = SSH.Local) { override def toString: String = path.toString def etc: Path = path + Path.basic("etc") @@ -188,15 +189,16 @@ def create(progress: Progress = new Progress): Directory = { progress.echo("Creating component directory " + path) - Isabelle_System.new_directory(path) - Isabelle_System.make_directory(etc) + ssh.new_directory(path) + ssh.make_directory(etc) this } - def ok: Boolean = settings.is_file || components.is_file || Sessions.is_session_dir(path) + def ok: Boolean = + ssh.is_file(settings) || ssh.is_file(components) || Sessions.is_session_dir(path, ssh = ssh) def check: Directory = - if (!path.is_dir) error("Bad component directory: " + path) + if (!ssh.is_dir(path)) error("Bad component directory: " + path) else if (!ok) { error("Malformed component directory: " + path + "\n (missing \"etc/settings\" or \"etc/components\" or \"ROOT\" or \"ROOTS\")") @@ -204,12 +206,12 @@ else this def read_components(): List[String] = - split_lines(File.read(components)).filter(_.nonEmpty) + split_lines(ssh.read(components)).filter(_.nonEmpty) def write_components(lines: List[String]): Unit = - File.write(components, terminate_lines(lines)) + ssh.write(components, terminate_lines(lines)) def write_settings(text: String): Unit = - File.write(settings, "# -*- shell-script -*- :mode=shellscript:\n" + text) + ssh.write(settings, "# -*- shell-script -*- :mode=shellscript:\n" + text) } diff -r f513f754c026 -r 34178d26a360 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Thu Mar 30 12:56:29 2023 +0200 +++ b/src/Pure/Thy/sessions.scala Thu Mar 30 14:25:31 2023 +0200 @@ -1255,8 +1255,8 @@ /* load sessions from certain directories */ - def is_session_dir(dir: Path): Boolean = - (dir + ROOT).is_file || (dir + ROOTS).is_file + def is_session_dir(dir: Path, ssh: SSH.System = SSH.Local): Boolean = + ssh.is_file(dir + ROOT) || ssh.is_file(dir + ROOTS) def check_session_dir(dir: Path): Path = if (is_session_dir(dir)) File.pwd() + dir.expand @@ -1266,7 +1266,7 @@ } def directories(dirs: List[Path], select_dirs: List[Path]): List[(Boolean, Path)] = { - val default_dirs = Components.directories().filter(is_session_dir) + val default_dirs = Components.directories().filter(is_session_dir(_)) for { (select, dir) <- (default_dirs ::: dirs).map((false, _)) ::: select_dirs.map((true, _)) } yield (select, dir.canonical) }