formal platform information, notably for ssh;

--- a/src/Pure/General/ssh.scala	Tue Sep 29 15:38:21 2020 +0200
+++ b/src/Pure/General/ssh.scala	Tue Sep 29 19:49:25 2020 +0200
@@ -463,6 +463,8 @@
         strict: Boolean = true): Process_Result =
       exec(command).result(progress_stdout, progress_stderr, strict)
 
+    override def isabelle_platform: Isabelle_Platform = Isabelle_Platform.remote(this)
+
 
     /* tmp dirs */
 
@@ -482,7 +484,6 @@
   }
 
 
-
   /* system operations */
 
   trait System
@@ -501,6 +502,8 @@
         strict: Boolean = true): Process_Result =
       Isabelle_System.bash(command, progress_stdout = progress_stdout,
         progress_stderr = progress_stderr, strict = strict)
+
+    def isabelle_platform: Isabelle_Platform = Isabelle_Platform.local()
   }
 
   object Local extends System

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/isabelle_platform.scala	Tue Sep 29 19:49:25 2020 +0200
@@ -0,0 +1,56 @@
+/*  Title:      Pure/System/isabelle_platform.scala
+    Author:     Makarius
+
+General hardware and operating system type for Isabelle system tools.
+*/
+
+package isabelle
+
+
+object Isabelle_Platform
+{
+  val settings: List[String] =
+    List(
+      "ISABELLE_PLATFORM_FAMILY",
+      "ISABELLE_PLATFORM32",
+      "ISABELLE_PLATFORM64",
+      "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 =
+  {
+    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
+    val values =
+      result.out_lines.map(line =>
+        space_explode('=', line) match {
+          case List(a, b) => (a, b)
+          case _ => error("Bad output: " + quote(result.out))
+        })
+    new Isabelle_Platform(values)
+  }
+}
+
+class Isabelle_Platform private(values: List[(String, String)])
+{
+  private def get(name: String): String =
+    values.collectFirst({ case (a, b) if a == name => b }).
+      getOrElse(error("Bad platform settings variable: " + quote(name)))
+
+  val ISABELLE_PLATFORM_FAMILY: String = get("ISABELLE_PLATFORM_FAMILY")
+  val ISABELLE_PLATFORM32: String = get("ISABELLE_PLATFORM32")
+  val ISABELLE_PLATFORM64: String = get("ISABELLE_PLATFORM64")
+  val ISABELLE_WINDOWS_PLATFORM32: String = get("ISABELLE_WINDOWS_PLATFORM32")
+  val ISABELLE_WINDOWS_PLATFORM64: String = get("ISABELLE_WINDOWS_PLATFORM64")
+
+  val is_linux: Boolean = ISABELLE_PLATFORM_FAMILY == "linux"
+  val is_macos: Boolean = ISABELLE_PLATFORM_FAMILY == "macos"
+  val is_windows: Boolean = ISABELLE_PLATFORM_FAMILY == "windows"
+
+  override def toString: String = ISABELLE_PLATFORM_FAMILY
+}

--- a/src/Pure/build-jars	Tue Sep 29 15:38:21 2020 +0200
+++ b/src/Pure/build-jars	Tue Sep 29 19:49:25 2020 +0200
@@ -123,6 +123,7 @@
   src/Pure/System/getopts.scala
   src/Pure/System/isabelle_charset.scala
   src/Pure/System/isabelle_fonts.scala
+  src/Pure/System/isabelle_platform.scala
   src/Pure/System/isabelle_process.scala
   src/Pure/System/isabelle_system.scala
   src/Pure/System/isabelle_tool.scala