| changeset 27353 | 71c4dd53d4cb |
| parent 26881 | bb68f50644a9 |
| child 27665 | b9e54ba563b3 |
| 27352:8adeff7fd4bc | 27353:71c4dd53d4cb |
|---|---|
33 |
33 |
34 (* parse *) |
34 (* parse *) |
35 |
35 |
36 fun token_source pos src = |
36 fun token_source pos src = |
37 Symbol.source true src |
37 Symbol.source true src |
38 |> T.source (SOME false) OuterSyntax.get_lexicons pos; |
38 |> T.source (SOME false) OuterKeyword.get_lexicons pos; |
39 |
39 |
40 fun parse_tokens pos src = Source.exhaust (token_source pos src); |
40 fun parse_tokens pos src = Source.exhaust (token_source pos src); |
41 |
41 |
42 |
42 |
43 (* present *) |
43 (* present *) |