equal
deleted
inserted
replaced
70 |
70 |
71 /* explode */ |
71 /* explode */ |
72 |
72 |
73 private def explode_elem(s: String): Elem = |
73 private def explode_elem(s: String): Elem = |
74 if (s == "..") Parent |
74 if (s == "..") Parent |
75 else if (s == "~") Variable("HOME") |
75 else if (s == "~") Variable("USER_HOME") |
76 else if (s == "~~") Variable("ISABELLE_HOME") |
76 else if (s == "~~") Variable("ISABELLE_HOME") |
77 else if (s.startsWith("$")) variable_elem(s.substring(1)) |
77 else if (s.startsWith("$")) variable_elem(s.substring(1)) |
78 else basic_elem(s) |
78 else basic_elem(s) |
79 |
79 |
80 private def explode_elems(ss: List[String]): List[Elem] = |
80 private def explode_elems(ss: List[String]): List[Elem] = |