--- 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 */
--- 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 =
--- 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))
}