--- a/src/Pure/Admin/other_isabelle.scala Wed Jan 25 14:51:13 2023 +0100
+++ b/src/Pure/Admin/other_isabelle.scala Wed Jan 25 14:58:34 2023 +0100
@@ -10,24 +10,33 @@
object Other_Isabelle {
def apply(
- isabelle_home: Path,
+ root: Path,
isabelle_identifier: String = "",
+ ssh: SSH.System = SSH.Local,
progress: Progress = new Progress
): Other_Isabelle = {
- if (proper_string(System.getenv("ISABELLE_SETTINGS_PRESENT")).isDefined) {
- error("Cannot initialize with enclosing ISABELLE_SETTINGS_PRESENT")
- }
-
- new Other_Isabelle(isabelle_home.canonical, isabelle_identifier, progress)
+ val (isabelle_home, url_prefix) =
+ ssh match {
+ case session: SSH.Session => (ssh.absolute_path(root), session.rsync_prefix)
+ case _ =>
+ if (proper_string(System.getenv("ISABELLE_SETTINGS_PRESENT")).isDefined) {
+ error("Cannot manage other Isabelle distribution: global ISABELLE_SETTINGS_PRESENT")
+ }
+ (root.canonical, "")
+ }
+ val isabelle_home_url = url_prefix + isabelle_home.implode
+ new Other_Isabelle(isabelle_home, isabelle_identifier, isabelle_home_url, ssh, progress)
}
}
final class Other_Isabelle private(
val isabelle_home: Path,
val isabelle_identifier: String,
+ isabelle_home_url: String,
+ ssh: SSH.System,
progress: Progress
) {
- override def toString: String = isabelle_home.toString
+ override def toString: String = isabelle_home_url
/* static system */
@@ -38,9 +47,14 @@
echo: Boolean = false,
strict: Boolean = true
): Process_Result = {
- progress.bash(
- Isabelle_System.export_isabelle_identifier(isabelle_identifier) + script,
- env = null, cwd = isabelle_home.file, redirect = redirect, echo = echo, strict = strict)
+ ssh.execute(
+ Isabelle_System.export_isabelle_identifier(isabelle_identifier) +
+ "cd " + ssh.bash_path(isabelle_home) + "\n" + script,
+ progress_stdout = progress.echo_if(echo, _),
+ progress_stderr = progress.echo_if(echo, _),
+ redirect = redirect,
+ settings = false,
+ strict = strict)
}
def getenv(name: String): String =
@@ -57,27 +71,19 @@
def etc_settings: Path = etc + Path.explode("settings")
def etc_preferences: Path = etc + Path.explode("preferences")
- def resolve_components(echo: Boolean = false): Unit = {
- val missing = Path.split(getenv("ISABELLE_COMPONENTS_MISSING"))
- for (path <- missing) {
- Components.resolve(path.dir, path.file_name,
- progress = if (echo) progress else new Progress)
- }
- }
-
def scala_build(fresh: Boolean = false, echo: Boolean = false): Unit = {
- if (fresh) {
- Isabelle_System.rm_tree(isabelle_home + Path.explode("lib/classes"))
- }
+ if (fresh) ssh.rm_tree(isabelle_home + Path.explode("lib/classes"))
val dummy_stty = Path.explode("~~/lib/dummy_stty/stty")
- if (!expand_path(dummy_stty).is_file) {
- Isabelle_System.copy_file(dummy_stty,
- Isabelle_System.make_directory(expand_path(dummy_stty.dir)))
+ val dummy_stty_remote = expand_path(dummy_stty)
+ if (!ssh.is_file(dummy_stty_remote)) {
+ ssh.make_directory(dummy_stty_remote.dir)
+ ssh.write_file(dummy_stty_remote, dummy_stty)
+ ssh.set_executable(dummy_stty_remote, true)
}
try {
bash(
- "export PATH=\"" + bash_path(dummy_stty.dir) + ":$PATH\"\n" +
+ "export PATH=\"" + bash_path(dummy_stty_remote.dir) + ":$PATH\"\n" +
"export CLASSPATH=" + Bash.string(getenv("ISABELLE_CLASSPATH")) + "\n" +
"bin/isabelle jedit -b", echo = echo).check
}
@@ -102,21 +108,29 @@
"init_component " + quote(components_base) + "/" + name)
}
+ def resolve_components(echo: Boolean = false): Unit = {
+ val missing = Path.split(getenv("ISABELLE_COMPONENTS_MISSING"))
+ for (path <- missing) {
+ Components.resolve(path.dir, path.file_name, ssh = ssh,
+ progress = if (echo) progress else new Progress)
+ }
+ }
+
/* settings */
def clean_settings(): Boolean =
- if (!etc_settings.is_file) true
- else if (File.read(etc_settings).startsWith("# generated by Isabelle")) {
- etc_settings.file.delete
+ if (!ssh.is_file(etc_settings)) true
+ else if (ssh.read(etc_settings).startsWith("# generated by Isabelle")) {
+ ssh.delete(etc_settings)
true
}
else false
def init_settings(settings: List[String]): Unit = {
if (clean_settings()) {
- Isabelle_System.make_directory(etc_settings.dir)
- File.write(etc_settings,
+ ssh.make_directory(etc_settings.dir)
+ ssh.write(etc_settings,
"# generated by Isabelle " + Date.now() + "\n" +
"#-*- shell-script -*- :mode=shellscript:\n" +
settings.mkString("\n", "\n", "\n"))
@@ -129,7 +143,7 @@
def cleanup(): Unit = {
clean_settings()
- etc.file.delete
- isabelle_home_user.file.delete
+ ssh.delete(etc)
+ ssh.delete(isabelle_home_user)
}
}