equal
deleted
inserted
replaced
94 |
94 |
95 fun err (toks, None) = kind ^ get_pos toks |
95 fun err (toks, None) = kind ^ get_pos toks |
96 | err (toks, Some msg) = kind ^ get_pos toks ^ ": " ^ msg; |
96 | err (toks, Some msg) = kind ^ get_pos toks ^ ": " ^ msg; |
97 in Scan.!! err scan end; |
97 in Scan.!! err scan end; |
98 |
98 |
99 val !!! = cut "Outer syntax error"; |
99 fun !!! scan = cut "Outer syntax error" scan; |
100 val !!!! = cut "Corrupted outer syntax in presentation"; |
100 fun !!!! scan = cut "Corrupted outer syntax in presentation" scan; |
101 |
101 |
102 |
102 |
103 |
103 |
104 (** basic parsers **) |
104 (** basic parsers **) |
105 |
105 |