# HG changeset patch # User wenzelm # Date 1606659798 -3600 # Node ID 93b50b9e3494589625952e0812f262ac8884ad93 # Parent a9ef3904111407416da55d8edbf15ee0a3545702 clarified checks (see f34f5c057c9e); diff -r a9ef39041114 -r 93b50b9e3494 src/Pure/PIDE/resources.scala --- a/src/Pure/PIDE/resources.scala Sun Nov 29 14:57:15 2020 +0100 +++ b/src/Pure/PIDE/resources.scala Sun Nov 29 15:23:18 2020 +0100 @@ -221,7 +221,7 @@ { if (node_name.is_theory && reader.source.length > 0) { try { - val header = Thy_Header.read(reader, start, strict).check_keywords + val header = Thy_Header.read(reader, start, strict) val base_name = node_name.theory_base_name if (Long_Name.is_qualified(header.name)) { diff -r a9ef39041114 -r 93b50b9e3494 src/Pure/Thy/thy_header.scala --- 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 } }