--- a/src/Pure/System/isabelle_platform.scala Mon May 05 17:04:14 2025 +0100
+++ b/src/Pure/System/isabelle_platform.scala Tue May 06 16:52:39 2025 +0200
@@ -16,22 +16,18 @@
"ISABELLE_WINDOWS_PLATFORM64",
"ISABELLE_APPLE_PLATFORM64")
- def apply(ssh: Option[SSH.Session] = None): Isabelle_Platform = {
- ssh match {
- case None =>
- new Isabelle_Platform(settings.map(a => (a, Isabelle_System.getenv(a))))
- case Some(ssh) =>
- val script =
- File.read(Path.explode("~~/lib/scripts/isabelle-platform")) + "\n" +
- settings.map(a => "echo \"" + Bash.string(a) + "=$" + Bash.string(a) + "\"").mkString("\n")
- val result = ssh.execute("bash -c " + Bash.string(script)).check
- new Isabelle_Platform(
- result.out_lines.map(line =>
- Properties.Eq.unapply(line) getOrElse error("Bad output: " + quote(result.out))))
- }
+ lazy val local: Isabelle_Platform =
+ new Isabelle_Platform(settings.map(a => (a, Isabelle_System.getenv(a))))
+
+ def remote(ssh: SSH.Session): Isabelle_Platform = {
+ val script =
+ File.read(Path.explode("~~/lib/scripts/isabelle-platform")) + "\n" +
+ settings.map(a => "echo \"" + Bash.string(a) + "=$" + Bash.string(a) + "\"").mkString("\n")
+ val result = ssh.execute("bash -c " + Bash.string(script)).check
+ new Isabelle_Platform(
+ result.out_lines.map(line =>
+ Properties.Eq.unapply(line) getOrElse error("Bad output: " + quote(result.out))))
}
-
- lazy val self: Isabelle_Platform = apply()
}
class Isabelle_Platform private(val settings: List[(String, String)]) {