--- a/src/Pure/System/isabelle_platform.scala Tue Sep 29 19:54:59 2020 +0200
+++ b/src/Pure/System/isabelle_platform.scala Tue Sep 29 20:00:59 2020 +0200
@@ -17,21 +17,23 @@
"ISABELLE_WINDOWS_PLATFORM32",
"ISABELLE_WINDOWS_PLATFORM64")
- def local(): Isabelle_Platform =
- new Isabelle_Platform(settings.map(a => (a, Isabelle_System.getenv(a))))
-
- def remote(ssh: SSH.Session): Isabelle_Platform =
+ def apply(ssh: Option[SSH.Session] = None): 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 =>
- space_explode('=', line) match {
- case List(a, b) => (a, b)
- case _ => error("Bad output: " + quote(result.out))
- }))
+ 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 =>
+ space_explode('=', line) match {
+ case List(a, b) => (a, b)
+ case _ => error("Bad output: " + quote(result.out))
+ }))
+ }
}
}