--- 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))
--- 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))
--- 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))
--- 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))
--- 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))
--- 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
) {
--- 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))
--- 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))
--- 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))
--- 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))
--- 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())
--- 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))
--- 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)
--- 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)]) {
--- 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")
--- 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")