src/Pure/Thy/thy_header.ML
changeset 67139 8fe0aba577af
parent 67136 1368cfa92b7a
child 67164 39f57f0757f1
     1.1 --- a/src/Pure/Thy/thy_header.ML	Tue Dec 05 15:29:37 2017 +0100
     1.2 +++ b/src/Pure/Thy/thy_header.ML	Tue Dec 05 15:55:14 2017 +0100
     1.3 @@ -77,15 +77,15 @@
     1.4       ((importsN, \<^here>), Keyword.quasi_command_spec),
     1.5       ((keywordsN, \<^here>), Keyword.quasi_command_spec),
     1.6       ((abbrevsN, \<^here>), Keyword.quasi_command_spec),
     1.7 -     ((chapterN, \<^here>), ((Keyword.document_heading, []), [])),
     1.8 -     ((sectionN, \<^here>), ((Keyword.document_heading, []), [])),
     1.9 -     ((subsectionN, \<^here>), ((Keyword.document_heading, []), [])),
    1.10 -     ((subsubsectionN, \<^here>), ((Keyword.document_heading, []), [])),
    1.11 -     ((paragraphN, \<^here>), ((Keyword.document_heading, []), [])),
    1.12 -     ((subparagraphN, \<^here>), ((Keyword.document_heading, []), [])),
    1.13 -     ((textN, \<^here>), ((Keyword.document_body, []), [])),
    1.14 -     ((txtN, \<^here>), ((Keyword.document_body, []), [])),
    1.15 -     ((text_rawN, \<^here>), ((Keyword.document_raw, []), [])),
    1.16 +     ((chapterN, \<^here>), Keyword.document_heading_spec),
    1.17 +     ((sectionN, \<^here>), Keyword.document_heading_spec),
    1.18 +     ((subsectionN, \<^here>), Keyword.document_heading_spec),
    1.19 +     ((subsubsectionN, \<^here>), Keyword.document_heading_spec),
    1.20 +     ((paragraphN, \<^here>), Keyword.document_heading_spec),
    1.21 +     ((subparagraphN, \<^here>), Keyword.document_heading_spec),
    1.22 +     ((textN, \<^here>), Keyword.document_body_spec),
    1.23 +     ((txtN, \<^here>), Keyword.document_body_spec),
    1.24 +     ((text_rawN, \<^here>), ((Keyword.document_raw, []), ["document"])),
    1.25       ((theoryN, \<^here>), ((Keyword.thy_begin, []), ["theory"])),
    1.26       (("ML", \<^here>), ((Keyword.thy_decl, []), ["ML"]))];
    1.27