22 private case class Basic(val name: String) extends Elem |
22 private case class Basic(val name: String) extends Elem |
23 private case class Variable(val name: String) extends Elem |
23 private case class Variable(val name: String) extends Elem |
24 private case object Parent extends Elem |
24 private case object Parent extends Elem |
25 |
25 |
26 private def err_elem(msg: String, s: String): Nothing = |
26 private def err_elem(msg: String, s: String): Nothing = |
27 error (msg + " path element specification: " + quote(s)) |
27 error (msg + " path element specification " + quote(s)) |
28 |
28 |
29 private def check_elem(s: String): String = |
29 private def check_elem(s: String): String = |
30 if (s == "" || s == "~" || s == "~~") err_elem("Illegal", s) |
30 if (s == "" || s == "~" || s == "~~") err_elem("Illegal", s) |
31 else |
31 else { |
32 s.iterator.filter(c => |
32 "/\\$:\"'".iterator.foreach(c => |
33 c == '/' || c == '\\' || c == '$' || c == ':' || c == '"' || c == '\'').toList match { |
33 if (s.iterator.exists(_ == c)) |
34 case Nil => s |
34 err_elem("Illegal character " + quote(c.toString) + " in", s)) |
35 case bads => |
35 s |
36 err_elem ("Illegal character(s) " + commas_quote(bads.map(_.toString)) + " in", s) |
36 } |
37 } |
|
38 |
37 |
39 private def root_elem(s: String): Elem = Root(check_elem(s)) |
38 private def root_elem(s: String): Elem = Root(check_elem(s)) |
40 private def basic_elem(s: String): Elem = Basic(check_elem(s)) |
39 private def basic_elem(s: String): Elem = Basic(check_elem(s)) |
41 private def variable_elem(s: String): Elem = Variable(check_elem(s)) |
40 private def variable_elem(s: String): Elem = Variable(check_elem(s)) |
42 |
41 |
71 val parent: Path = new Path(List(Parent)) |
70 val parent: Path = new Path(List(Parent)) |
72 |
71 |
73 |
72 |
74 /* explode */ |
73 /* explode */ |
75 |
74 |
76 private def explode_elem(s: String): Elem = |
|
77 if (s == "..") Parent |
|
78 else if (s == "~") Variable("USER_HOME") |
|
79 else if (s == "~~") Variable("ISABELLE_HOME") |
|
80 else if (s.startsWith("$")) variable_elem(s.substring(1)) |
|
81 else basic_elem(s) |
|
82 |
|
83 private def explode_elems(ss: List[String]): List[Elem] = |
|
84 ss.filterNot(s => s.isEmpty || s == ".").map(explode_elem).reverse |
|
85 |
|
86 def explode(str: String): Path = |
75 def explode(str: String): Path = |
87 { |
76 { |
|
77 def explode_elem(s: String): Elem = |
|
78 try { |
|
79 if (s == "..") Parent |
|
80 else if (s == "~") Variable("USER_HOME") |
|
81 else if (s == "~~") Variable("ISABELLE_HOME") |
|
82 else if (s.startsWith("$")) variable_elem(s.substring(1)) |
|
83 else basic_elem(s) |
|
84 } |
|
85 catch { case ERROR(msg) => cat_error(msg, "The error(s) above occurred in " + quote(str)) } |
|
86 |
88 val ss = space_explode('/', str) |
87 val ss = space_explode('/', str) |
89 val r = ss.takeWhile(_.isEmpty).length |
88 val r = ss.takeWhile(_.isEmpty).length |
90 val es = ss.dropWhile(_.isEmpty) |
89 val es = ss.dropWhile(_.isEmpty) |
91 val (roots, raw_elems) = |
90 val (roots, raw_elems) = |
92 if (r == 0) (Nil, es) |
91 if (r == 0) (Nil, es) |
93 else if (r == 1) (List(Root("")), es) |
92 else if (r == 1) (List(Root("")), es) |
94 else if (es.isEmpty) (List(Root("")), Nil) |
93 else if (es.isEmpty) (List(Root("")), Nil) |
95 else (List(root_elem(es.head)), es.tail) |
94 else (List(root_elem(es.head)), es.tail) |
96 new Path(norm_elems(explode_elems(raw_elems) ++ roots)) |
95 val elems = raw_elems.filterNot(s => s.isEmpty || s == ".").map(explode_elem) |
|
96 |
|
97 new Path(norm_elems(elems.reverse ++ roots)) |
97 } |
98 } |
98 |
99 |
99 def is_ok(str: String): Boolean = |
100 def is_ok(str: String): Boolean = |
100 try { explode(str); true } catch { case ERROR(_) => false } |
101 try { explode(str); true } catch { case ERROR(_) => false } |
101 |
102 |