equal
deleted
inserted
replaced
231 error("Illegal path variable nesting: " + s + "=" + path.toString) |
231 error("Illegal path variable nesting: " + s + "=" + path.toString) |
232 else path.elems |
232 else path.elems |
233 case x => List(x) |
233 case x => List(x) |
234 } |
234 } |
235 |
235 |
236 new Path(Path.norm_elems(elems.map(eval).flatten)) |
236 new Path(Path.norm_elems(elems.flatMap(eval))) |
237 } |
237 } |
238 |
238 |
239 def expand: Path = expand_env(Isabelle_System.settings()) |
239 def expand: Path = expand_env(Isabelle_System.settings()) |
240 |
240 |
241 def file_name: String = expand.base.implode |
241 def file_name: String = expand.base.implode |