equal
deleted
inserted
replaced
71 |
71 |
72 fun pos_of (Token ((pos, _), _)) = pos; |
72 fun pos_of (Token ((pos, _), _)) = pos; |
73 fun end_pos_of (Token ((_, pos), _)) = pos; |
73 fun end_pos_of (Token ((_, pos), _)) = pos; |
74 |
74 |
75 |
75 |
76 (* control tokens *) |
76 (* stopper *) |
77 |
77 |
78 fun mk_eof pos = Token ((pos, Position.none), (EOF, "")); |
78 fun mk_eof pos = Token ((pos, Position.none), (EOF, "")); |
79 val eof = mk_eof Position.none; |
79 val eof = mk_eof Position.none; |
80 |
80 |
81 fun is_eof (Token (_, (EOF, _))) = true |
81 fun is_eof (Token (_, (EOF, _))) = true |