| changeset 72773 | 93b50b9e3494 |
| parent 72765 | f34f5c057c9e |
| child 72774 | 51c0f79d6eed |
--- a/src/Pure/Thy/thy_header.scala Sun Nov 29 14:57:15 2020 +0100 +++ b/src/Pure/Thy/thy_header.scala Sun Nov 29 15:23:18 2020 +0100 @@ -221,7 +221,7 @@ val (drop_tokens, tokens) = read_tokens(Scan.char_reader(text), strict) val pos = (start /: drop_tokens)(_.advance(_)) - Parser.parse_header(tokens, pos) + Parser.parse_header(tokens, pos).check_keywords } }