22 private case class Basic(name: String) extends Elem |
22 private case class Basic(name: String) extends Elem |
23 private case class Variable(name: String) extends Elem |
23 private case class Variable(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 " + quote(s)) |
|
28 |
|
29 private val illegal_elem = Set("", "~", "~~") |
|
30 private val illegal_char = "/\\$:\"'" |
28 |
31 |
29 private def check_elem(s: String): String = |
32 private def check_elem(s: String): String = |
30 if (s == "" || s == "~" || s == "~~") err_elem("Illegal", s) |
33 if (illegal_elem.contains(s)) err_elem("Illegal", s) |
31 else { |
34 else { |
32 "/\\$:\"'".iterator.foreach(c => |
35 for (c <- illegal_char if s.contains(c)) { |
33 if (s.iterator.contains(c)) |
36 err_elem("Illegal character " + quote(c.toString) + " in", s) |
34 err_elem("Illegal character " + quote(c.toString) + " in", s)) |
37 } |
35 s |
38 s |
36 } |
39 } |
37 |
40 |
38 private def root_elem(s: String): Elem = Root(check_elem(s)) |
41 private def root_elem(s: String): Elem = Root(check_elem(s)) |
39 private def basic_elem(s: String): Elem = Basic(check_elem(s)) |
42 private def basic_elem(s: String): Elem = Basic(check_elem(s)) |