# HG changeset patch # User wenzelm # Date 1468255170 -7200 # Node ID 998acd66fbd789503bbb349ff8c5e53ca51d46bc # Parent 55b1bed86c44c2dfa9891ed217b6444c7f5d390d clarified keywords; diff -r 55b1bed86c44 -r 998acd66fbd7 src/Pure/Thy/thy_header.ML --- a/src/Pure/Thy/thy_header.ML Mon Jul 11 18:30:07 2016 +0200 +++ b/src/Pure/Thy/thy_header.ML Mon Jul 11 18:39:30 2016 +0200 @@ -71,8 +71,8 @@ (("==", @{here}), Keyword.no_spec), (("and", @{here}), Keyword.no_spec), ((beginN, @{here}), Keyword.no_spec), - ((importsN, @{here}), Keyword.no_spec), - ((keywordsN, @{here}), Keyword.no_spec), + ((importsN, @{here}), Keyword.quasi_command_spec), + ((keywordsN, @{here}), Keyword.quasi_command_spec), ((chapterN, @{here}), ((Keyword.document_heading, []), [])), ((sectionN, @{here}), ((Keyword.document_heading, []), [])), ((subsectionN, @{here}), ((Keyword.document_heading, []), [])), diff -r 55b1bed86c44 -r 998acd66fbd7 src/Pure/Thy/thy_header.scala --- a/src/Pure/Thy/thy_header.scala Mon Jul 11 18:30:07 2016 +0200 +++ b/src/Pure/Thy/thy_header.scala Mon Jul 11 18:39:30 2016 +0200 @@ -45,8 +45,8 @@ ("==", Keyword.no_spec, None), (AND, Keyword.no_spec, None), (BEGIN, Keyword.no_spec, None), - (IMPORTS, Keyword.no_spec, None), - (KEYWORDS, Keyword.no_spec, None), + (IMPORTS, Keyword.quasi_command_spec, None), + (KEYWORDS, Keyword.quasi_command_spec, None), (CHAPTER, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None), (SECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None), (SUBSECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),