# HG changeset patch
# User wenzelm
# Date 1476551312 -7200
# Node ID b46969a851a94fbf381c7075cbaf923e24f6c39c
# Parent  cc2edb86f3ccf287e2e2e16110c309fd2edd161c
expand relatively to given environment, notably remote HOME;

diff -r cc2edb86f3cc -r b46969a851a9 src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Sat Oct 15 16:35:50 2016 +0200
+++ b/src/Pure/General/path.scala	Sat Oct 15 19:08:32 2016 +0200
@@ -182,12 +182,12 @@
 
   /* expand */
 
-  def expand: Path =
+  def expand_env(env: Map[String, String]): Path =
   {
     def eval(elem: Path.Elem): List[Path.Elem] =
       elem match {
         case Path.Variable(s) =>
-          val path = Path.explode(Isabelle_System.getenv_strict(s))
+          val path = Path.explode(Isabelle_System.getenv_strict(s, env))
           if (path.elems.exists(_.isInstanceOf[Path.Variable]))
             error("Illegal path variable nesting: " + s + "=" + path.toString)
           else path.elems
@@ -197,6 +197,8 @@
     new Path(Path.norm_elems(elems.map(eval).flatten))
   }
 
+  def expand: Path = expand_env(Isabelle_System.settings())
+
 
   /* source position */
 
diff -r cc2edb86f3cc -r b46969a851a9 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Sat Oct 15 16:35:50 2016 +0200
+++ b/src/Pure/General/ssh.scala	Sat Oct 15 19:08:32 2016 +0200
@@ -129,7 +129,12 @@
   {
     channel.connect(connect_timeout(session.options))
 
-    def home: String = channel.getHome()
+    val settings: Map[String, String] =
+    {
+      val home = channel.getHome
+      Map("HOME" -> home, "USER_HOME" -> home)
+    }
+    def path(p: Path): String = p.expand_env(settings).implode
 
     def chmod(permissions: Int, remote_path: String) { channel.chmod(permissions, remote_path) }
     def mv(remote_path1: String, remote_path2: String): Unit =
diff -r cc2edb86f3cc -r b46969a851a9 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Sat Oct 15 16:35:50 2016 +0200
+++ b/src/Pure/System/isabelle_system.scala	Sat Oct 15 19:08:32 2016 +0200
@@ -133,11 +133,12 @@
 
   /* getenv */
 
-  def getenv(name: String): String = settings().getOrElse(name, "")
+  def getenv(name: String, env: Map[String, String] = settings()): String =
+    env.getOrElse(name, "")
 
-  def getenv_strict(name: String): String =
+  def getenv_strict(name: String, env: Map[String, String] = settings()): String =
   {
-    val value = getenv(name)
+    val value = getenv(name, env)
     if (value != "") value
     else error("Undefined Isabelle environment variable: " + quote(name))
   }