# HG changeset patch
# User wenzelm
# Date 1601402099 -7200
# Node ID 626920749f5d42983d8e3a02e32c5643675f8f8a
# Parent  54871a086193df6bf3abdc514cdc69520fb36aee
tuned signature;

diff -r 54871a086193 -r 626920749f5d src/Pure/System/isabelle_platform.scala
--- a/src/Pure/System/isabelle_platform.scala	Tue Sep 29 19:49:25 2020 +0200
+++ b/src/Pure/System/isabelle_platform.scala	Tue Sep 29 19:54:59 2020 +0200
@@ -26,20 +26,19 @@
       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 =
+    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))
-        })
-    new Isabelle_Platform(values)
+        }))
   }
 }
 
-class Isabelle_Platform private(values: List[(String, String)])
+class Isabelle_Platform private(val settings: List[(String, String)])
 {
   private def get(name: String): String =
-    values.collectFirst({ case (a, b) if a == name => b }).
+    settings.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")