# HG changeset patch
# User wenzelm
# Date 1746543159 -7200
# Node ID 3133f9748ea82289901367d2400013a0e9b2edee
# Parent  5540532087fa9372066d79b883e34942ae2210d2
clarified signature;

diff -r 5540532087fa -r 3133f9748ea8 src/Pure/Admin/component_bash_process.scala
--- a/src/Pure/Admin/component_bash_process.scala	Mon May 05 17:04:14 2025 +0100
+++ b/src/Pure/Admin/component_bash_process.scala	Tue May 06 16:52:39 2025 +0200
@@ -39,7 +39,7 @@
 
     /* platform */
 
-    val platform_name = Isabelle_Platform.self.ISABELLE_PLATFORM(apple = true)
+    val platform_name = Isabelle_Platform.local.ISABELLE_PLATFORM(apple = true)
     val platform_dir =
       Isabelle_System.make_directory(component_dir.path + Path.basic(platform_name))
 
diff -r 5540532087fa -r 3133f9748ea8 src/Pure/Admin/component_csdp.scala
--- a/src/Pure/Admin/component_csdp.scala	Mon May 05 17:04:14 2025 +0100
+++ b/src/Pure/Admin/component_csdp.scala	Tue May 06 16:52:39 2025 +0200
@@ -80,7 +80,7 @@
 
       /* platform */
 
-      val platform_name = Isabelle_Platform.self.ISABELLE_PLATFORM(windows = true)
+      val platform_name = Isabelle_Platform.local.ISABELLE_PLATFORM(windows = true)
       val platform_dir =
         Isabelle_System.make_directory(component_dir.path + Path.basic(platform_name))
 
diff -r 5540532087fa -r 3133f9748ea8 src/Pure/Admin/component_e.scala
--- a/src/Pure/Admin/component_e.scala	Mon May 05 17:04:14 2025 +0100
+++ b/src/Pure/Admin/component_e.scala	Tue May 06 16:52:39 2025 +0200
@@ -26,7 +26,7 @@
       val component_dir =
         Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress)
 
-      val platform_name = Isabelle_Platform.self.ISABELLE_PLATFORM(apple = true)
+      val platform_name = Isabelle_Platform.local.ISABELLE_PLATFORM(apple = true)
       val platform_dir =
         Isabelle_System.make_directory(component_dir.path + Path.basic(platform_name))
 
diff -r 5540532087fa -r 3133f9748ea8 src/Pure/Admin/component_hol_light.scala
--- a/src/Pure/Admin/component_hol_light.scala	Mon May 05 17:04:14 2025 +0100
+++ b/src/Pure/Admin/component_hol_light.scala	Tue May 06 16:52:39 2025 +0200
@@ -48,7 +48,7 @@
     val component_dir =
       Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress)
 
-    val platform = Isabelle_Platform.self.ISABELLE_PLATFORM(windows = true, apple = true)
+    val platform = Isabelle_Platform.local.ISABELLE_PLATFORM(windows = true, apple = true)
     val platform_dir = Isabelle_System.make_directory(component_dir.path + Path.basic(platform))
 
 
diff -r 5540532087fa -r 3133f9748ea8 src/Pure/Admin/component_minisat.scala
--- a/src/Pure/Admin/component_minisat.scala	Mon May 05 17:04:14 2025 +0100
+++ b/src/Pure/Admin/component_minisat.scala	Tue May 06 16:52:39 2025 +0200
@@ -46,7 +46,7 @@
 
       /* platform */
 
-      val platform_name = Isabelle_Platform.self.ISABELLE_PLATFORM()
+      val platform_name = Isabelle_Platform.local.ISABELLE_PLATFORM()
       val platform_dir =
         Isabelle_System.make_directory(component_dir.path + Path.basic(platform_name))
 
diff -r 5540532087fa -r 3133f9748ea8 src/Pure/Admin/component_polyml.scala
--- a/src/Pure/Admin/component_polyml.scala	Mon May 05 17:04:14 2025 +0100
+++ b/src/Pure/Admin/component_polyml.scala	Tue May 06 16:52:39 2025 +0200
@@ -18,7 +18,7 @@
     libs: Set[String] = Set.empty)
 
   sealed case class Platform_Context(
-    platform: Isabelle_Platform = Isabelle_Platform.self,
+    platform: Isabelle_Platform = Isabelle_Platform.local,
     mingw: MinGW = MinGW.none,
     progress: Progress = new Progress
   ) {
diff -r 5540532087fa -r 3133f9748ea8 src/Pure/Admin/component_rsync.scala
--- a/src/Pure/Admin/component_rsync.scala	Mon May 05 17:04:14 2025 +0100
+++ b/src/Pure/Admin/component_rsync.scala	Tue May 06 16:52:39 2025 +0200
@@ -50,7 +50,7 @@
           .create(progress = progress)
           .write_platforms()
 
-      val platform_name = Isabelle_Platform.self.ISABELLE_PLATFORM(apple = true)
+      val platform_name = Isabelle_Platform.local.ISABELLE_PLATFORM(apple = true)
       val platform_dir =
         Isabelle_System.make_directory(component_dir.path + Path.basic(platform_name))
 
diff -r 5540532087fa -r 3133f9748ea8 src/Pure/Admin/component_spass.scala
--- a/src/Pure/Admin/component_spass.scala	Mon May 05 17:04:14 2025 +0100
+++ b/src/Pure/Admin/component_spass.scala	Tue May 06 16:52:39 2025 +0200
@@ -54,7 +54,7 @@
       val component_dir =
         Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress)
 
-      val platform_name = Isabelle_Platform.self.ISABELLE_PLATFORM()
+      val platform_name = Isabelle_Platform.local.ISABELLE_PLATFORM()
       val platform_dir =
         Isabelle_System.make_directory(component_dir.path + Path.basic(platform_name))
 
diff -r 5540532087fa -r 3133f9748ea8 src/Pure/Admin/component_vampire.scala
--- a/src/Pure/Admin/component_vampire.scala	Mon May 05 17:04:14 2025 +0100
+++ b/src/Pure/Admin/component_vampire.scala	Tue May 06 16:52:39 2025 +0200
@@ -48,7 +48,7 @@
 
       /* platform */
 
-      val platform_name = Isabelle_Platform.self.ISABELLE_PLATFORM()
+      val platform_name = Isabelle_Platform.local.ISABELLE_PLATFORM()
       val platform_dir =
         Isabelle_System.make_directory(component_dir.path + Path.basic(platform_name))
 
diff -r 5540532087fa -r 3133f9748ea8 src/Pure/Admin/component_verit.scala
--- a/src/Pure/Admin/component_verit.scala	Mon May 05 17:04:14 2025 +0100
+++ b/src/Pure/Admin/component_verit.scala	Tue May 06 16:52:39 2025 +0200
@@ -46,7 +46,7 @@
 
       /* platform */
 
-      val platform_name = Isabelle_Platform.self.ISABELLE_PLATFORM(windows = true)
+      val platform_name = Isabelle_Platform.local.ISABELLE_PLATFORM(windows = true)
       val platform_dir =
         Isabelle_System.make_directory(component_dir.path + Path.basic(platform_name))
 
diff -r 5540532087fa -r 3133f9748ea8 src/Pure/Admin/component_windows_app.scala
--- a/src/Pure/Admin/component_windows_app.scala	Mon May 05 17:04:14 2025 +0100
+++ b/src/Pure/Admin/component_windows_app.scala	Tue May 06 16:52:39 2025 +0200
@@ -12,7 +12,7 @@
 
   def tool_platform(): String = {
     require(Platform.is_unix, "Linux or macOS platform required")
-    Isabelle_Platform.self.ISABELLE_PLATFORM64
+    Isabelle_Platform.local.ISABELLE_PLATFORM64
   }
 
   def tool_platform_path(): Path = Path.basic(tool_platform())
diff -r 5540532087fa -r 3133f9748ea8 src/Pure/Admin/component_zipperposition.scala
--- a/src/Pure/Admin/component_zipperposition.scala	Mon May 05 17:04:14 2025 +0100
+++ b/src/Pure/Admin/component_zipperposition.scala	Tue May 06 16:52:39 2025 +0200
@@ -31,7 +31,7 @@
 
       /* platform */
 
-      val platform_name = Isabelle_Platform.self.ISABELLE_PLATFORM()
+      val platform_name = Isabelle_Platform.local.ISABELLE_PLATFORM()
       val platform_dir =
         Isabelle_System.make_directory(component_dir.path + Path.basic(platform_name))
 
diff -r 5540532087fa -r 3133f9748ea8 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Mon May 05 17:04:14 2025 +0100
+++ b/src/Pure/General/ssh.scala	Tue May 06 16:52:39 2025 +0200
@@ -255,7 +255,8 @@
         progress_stderr = progress.echo(_)).check
     }
 
-    override lazy val isabelle_platform: Isabelle_Platform = Isabelle_Platform(ssh = Some(ssh))
+    override lazy val isabelle_platform: Isabelle_Platform =
+      Isabelle_Platform.remote(ssh)
 
 
     /* remote file-system */
@@ -595,7 +596,7 @@
     def download_file(url_name: String, file: Path, progress: Progress = new Progress): Unit =
       Isabelle_System.download_file(url_name, file, progress = progress)
 
-    def isabelle_platform: Isabelle_Platform = Isabelle_Platform()
+    def isabelle_platform: Isabelle_Platform = Isabelle_Platform.local
 
     def isabelle_platform_family: Platform.Family =
       Platform.Family.parse(isabelle_platform.ISABELLE_PLATFORM_FAMILY)
diff -r 5540532087fa -r 3133f9748ea8 src/Pure/System/isabelle_platform.scala
--- 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)]) {
diff -r 5540532087fa -r 3133f9748ea8 src/Pure/Tools/dotnet_setup.scala
--- a/src/Pure/Tools/dotnet_setup.scala	Mon May 05 17:04:14 2025 +0100
+++ b/src/Pure/Tools/dotnet_setup.scala	Tue May 06 16:52:39 2025 +0200
@@ -36,7 +36,7 @@
   /* dotnet download and setup */
 
   def default_platform: String =
-    Isabelle_Platform.self.ISABELLE_PLATFORM(windows = true, apple = true)
+    Isabelle_Platform.local.ISABELLE_PLATFORM(windows = true, apple = true)
   def default_target_dir: Path = Components.default_components_base
   def default_install_url: String = "https://dot.net/v1/dotnet-install"
   def default_version: String = Isabelle_System.getenv_strict("ISABELLE_DOTNET_VERSION")
diff -r 5540532087fa -r 3133f9748ea8 src/Pure/Tools/go_setup.scala
--- a/src/Pure/Tools/go_setup.scala	Mon May 05 17:04:14 2025 +0100
+++ b/src/Pure/Tools/go_setup.scala	Tue May 06 16:52:39 2025 +0200
@@ -34,7 +34,7 @@
   /* Go download and setup */
 
   def default_platform: String =
-    Isabelle_Platform.self.ISABELLE_PLATFORM(windows = true, apple = true)
+    Isabelle_Platform.local.ISABELLE_PLATFORM(windows = true, apple = true)
   def default_target_dir: Path = Components.default_components_base
   val default_url = "https://go.dev/dl"
   def default_version: String = Isabelle_System.getenv_strict("ISABELLE_GO_VERSION")