equal
deleted
inserted
replaced
83 |
83 |
84 (* group atomic parsers (no cuts!) *) |
84 (* group atomic parsers (no cuts!) *) |
85 |
85 |
86 fun fail_with s = Scan.fail_with |
86 fun fail_with s = Scan.fail_with |
87 (fn [] => s ^ " expected (past end-of-file!)" |
87 (fn [] => s ^ " expected (past end-of-file!)" |
88 | (tok :: _) => s ^ " expected,\nbut " ^ T.name_of tok ^ " " ^ |
88 | (tok :: _) => s ^ " expected,\nbut " ^ T.name_of tok ^ T.pos_of tok ^ " was found"); |
89 quote (T.val_of tok) ^ T.pos_of tok ^ " was found"); |
|
90 |
89 |
91 fun group s scan = scan || fail_with s; |
90 fun group s scan = scan || fail_with s; |
92 |
91 |
93 |
92 |
94 (* cut *) |
93 (* cut *) |