equal
deleted
inserted
replaced
49 |
49 |
50 fun check_elem (chs as []) = err_elem "Illegal" chs |
50 fun check_elem (chs as []) = err_elem "Illegal" chs |
51 | check_elem (chs as ["~"]) = err_elem "Illegal" chs |
51 | check_elem (chs as ["~"]) = err_elem "Illegal" chs |
52 | check_elem (chs as ["~", "~"]) = err_elem "Illegal" chs |
52 | check_elem (chs as ["~", "~"]) = err_elem "Illegal" chs |
53 | check_elem chs = |
53 | check_elem chs = |
54 (case inter (op =) ["/", "\\", ":"] chs of |
54 (case inter (op =) ["/", "\\", "$", ":", "\"", "'"] chs of |
55 [] => chs |
55 [] => chs |
56 | bads => err_elem ("Illegal character(s) " ^ commas_quote bads ^ " in") chs); |
56 | bads => err_elem ("Illegal character(s) " ^ commas_quote bads ^ " in") chs); |
57 |
57 |
58 in |
58 in |
59 |
59 |