Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clarified checks (see f34f5c057c9e);
authorwenzelm
Sun, 29 Nov 2020 15:23:18 +0100
changeset 72773 93b50b9e3494
parent 72772 a9ef39041114
child 72774 51c0f79d6eed
clarified checks (see f34f5c057c9e);
src/Pure/PIDE/resources.scala file | annotate | diff | comparison | revisions
src/Pure/Thy/thy_header.scala file | annotate | diff | comparison | revisions 
--- 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)) {
--- 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
   }
 }
isabelle