equal
deleted
inserted
replaced
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 " + quote(s)) |
27 error(msg + " path element " + quote(s)) |
28 |
28 |
29 private val illegal_elem = Set("", "~", "~~", ".", "..") |
29 private val illegal_elem = Set("", "~", "~~", ".", "..") |
30 private val illegal_char = "/\\$:\"'" |
30 private val illegal_char = "/\\$:\"'<>|?*" |
31 |
31 |
32 private def check_elem(s: String): String = |
32 private def check_elem(s: String): String = |
33 if (illegal_elem.contains(s)) err_elem("Illegal", s) |
33 if (illegal_elem.contains(s)) err_elem("Illegal", s) |
34 else { |
34 else { |
35 for (c <- s if illegal_char.contains(c)) { |
35 for (c <- s) { |
36 err_elem("Illegal character " + quote(c.toString) + " in", s) |
36 if (c.toInt < 32) |
|
37 err_elem("Illegal control character " + c.toInt + " in", s) |
|
38 if (illegal_char.contains(c)) |
|
39 err_elem("Illegal character " + quote(c.toString) + " in", s) |
37 } |
40 } |
38 s |
41 s |
39 } |
42 } |
40 |
43 |
41 private def root_elem(s: String): Elem = Root(check_elem(s)) |
44 private def root_elem(s: String): Elem = Root(check_elem(s)) |