--- a/src/Pure/Thy/thy_header.ML Mon Jul 11 18:39:30 2016 +0200
+++ b/src/Pure/Thy/thy_header.ML Mon Jul 11 19:03:08 2016 +0200
@@ -70,7 +70,7 @@
(("::", @{here}), Keyword.no_spec),
(("==", @{here}), Keyword.no_spec),
(("and", @{here}), Keyword.no_spec),
- ((beginN, @{here}), Keyword.no_spec),
+ ((beginN, @{here}), Keyword.quasi_command_spec),
((importsN, @{here}), Keyword.quasi_command_spec),
((keywordsN, @{here}), Keyword.quasi_command_spec),
((chapterN, @{here}), ((Keyword.document_heading, []), [])),
--- a/src/Pure/Thy/thy_header.scala Mon Jul 11 18:39:30 2016 +0200
+++ b/src/Pure/Thy/thy_header.scala Mon Jul 11 19:03:08 2016 +0200
@@ -44,7 +44,7 @@
("::", Keyword.no_spec, None),
("==", Keyword.no_spec, None),
(AND, Keyword.no_spec, None),
- (BEGIN, Keyword.no_spec, None),
+ (BEGIN, Keyword.quasi_command_spec, None),
(IMPORTS, Keyword.quasi_command_spec, None),
(KEYWORDS, Keyword.quasi_command_spec, None),
(CHAPTER, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),