equal
deleted
inserted
replaced
137 |
137 |
138 def getenv(name: String, env: Map[String, String] = settings()): String = |
138 def getenv(name: String, env: Map[String, String] = settings()): String = |
139 env.getOrElse(name, "") |
139 env.getOrElse(name, "") |
140 |
140 |
141 def getenv_strict(name: String, env: Map[String, String] = settings()): String = |
141 def getenv_strict(name: String, env: Map[String, String] = settings()): String = |
142 { |
142 proper_string(getenv(name, env)) getOrElse |
143 val value = getenv(name, env) |
143 error("Undefined Isabelle environment variable: " + quote(name)) |
144 if (value != "") value |
|
145 else error("Undefined Isabelle environment variable: " + quote(name)) |
|
146 } |
|
147 |
144 |
148 def cygwin_root(): String = getenv_strict("CYGWIN_ROOT") |
145 def cygwin_root(): String = getenv_strict("CYGWIN_ROOT") |
149 |
146 |
150 def library_path(env: Map[String, String], elem: String): Map[String, String] = |
147 def library_path(env: Map[String, String], elem: String): Map[String, String] = |
151 if (Platform.is_windows) env |
148 if (Platform.is_windows) env |