clarified settings environment;
authorwenzelm
Sat Nov 11 16:28:15 2017 +0100 (6 months ago)
changeset 67046897f1ac84aab
parent 67045 6c94f749410a
child 67047 19b6091c2137
clarified settings environment;
src/Pure/Admin/other_isabelle.scala
     1.1 --- a/src/Pure/Admin/other_isabelle.scala	Sat Nov 11 16:01:02 2017 +0100
     1.2 +++ b/src/Pure/Admin/other_isabelle.scala	Sat Nov 11 16:28:15 2017 +0100
     1.3 @@ -10,18 +10,25 @@
     1.4  object Other_Isabelle
     1.5  {
     1.6    def apply(isabelle_home: Path,
     1.7 -      isabelle_identifier: String,
     1.8 +      isabelle_identifier: String = "",
     1.9 +      user_home: Path = Path.explode("$USER_HOME"),
    1.10        progress: Progress = No_Progress): Other_Isabelle =
    1.11 -    new Other_Isabelle(isabelle_home, isabelle_identifier, progress)
    1.12 +    new Other_Isabelle(isabelle_home, isabelle_identifier, user_home, progress)
    1.13  }
    1.14  
    1.15  class Other_Isabelle(
    1.16    val isabelle_home: Path,
    1.17    val isabelle_identifier: String,
    1.18 +  user_home: Path,
    1.19    progress: Progress)
    1.20  {
    1.21    other_isabelle =>
    1.22  
    1.23 +  override def toString: String = isabelle_home.toString
    1.24 +
    1.25 +  if (proper_string(System.getenv("ISABELLE_SETTINGS_PRESENT")).isDefined)
    1.26 +    error("Cannot initialize with enclosing ISABELLE_SETTINGS_PRESENT")
    1.27 +
    1.28  
    1.29    /* static system */
    1.30  
    1.31 @@ -30,7 +37,9 @@
    1.32        redirect: Boolean = false,
    1.33        echo: Boolean = false,
    1.34        strict: Boolean = true): Process_Result =
    1.35 -    progress.bash(Isabelle_System.export_isabelle_identifier(isabelle_identifier) + script,
    1.36 +    progress.bash(
    1.37 +      "export USER_HOME=" + File.bash_path(user_home) + "\n" +
    1.38 +      Isabelle_System.export_isabelle_identifier(isabelle_identifier) + script,
    1.39        env = null, cwd = isabelle_home.file, redirect = redirect, echo = echo, strict = strict)
    1.40  
    1.41    def apply(