# HG changeset patch
# User wenzelm
# Date 1601402459 -7200
# Node ID 676066aa47982b2529210e787a57f69d095d4806
# Parent  626920749f5d42983d8e3a02e32c5643675f8f8a
clarified signature;

diff -r 626920749f5d -r 676066aa4798 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Tue Sep 29 19:54:59 2020 +0200
+++ b/src/Pure/General/ssh.scala	Tue Sep 29 20:00:59 2020 +0200
@@ -463,7 +463,7 @@
         strict: Boolean = true): Process_Result =
       exec(command).result(progress_stdout, progress_stderr, strict)
 
-    override def isabelle_platform: Isabelle_Platform = Isabelle_Platform.remote(this)
+    override def isabelle_platform: Isabelle_Platform = Isabelle_Platform(ssh = Some(this))
 
 
     /* tmp dirs */
@@ -503,7 +503,7 @@
       Isabelle_System.bash(command, progress_stdout = progress_stdout,
         progress_stderr = progress_stderr, strict = strict)
 
-    def isabelle_platform: Isabelle_Platform = Isabelle_Platform.local()
+    def isabelle_platform: Isabelle_Platform = Isabelle_Platform()
   }
 
   object Local extends System
diff -r 626920749f5d -r 676066aa4798 src/Pure/System/isabelle_platform.scala
--- 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))
+            }))
+    }
   }
 }