src/Pure/Thy/thy_header.ML

 val headerN = "header";
 val chapterN = "chapter";
 val sectionN = "section";
 val subsectionN = "subsection";
 val subsubsectionN = "subsubsection";
+val textN = "text";
+val txtN = "txt";
+val text_rawN = "text_raw";
 
 val theoryN = "theory";
 val importsN = "imports";
 val keywordsN = "keywords";
 val beginN = "begin";

      ("==", NONE),
      ("and", NONE),
      (beginN, NONE),
      (importsN, NONE),
      (keywordsN, NONE),
-     (headerN, SOME ((Keyword.heading, []), [])),
-     (chapterN, SOME ((Keyword.heading, []), [])),
-     (sectionN, SOME ((Keyword.heading, []), [])),
-     (subsectionN, SOME ((Keyword.heading, []), [])),
-     (subsubsectionN, SOME ((Keyword.heading, []), [])),
+     (headerN, SOME ((Keyword.document_heading, []), [])),
+     (chapterN, SOME ((Keyword.document_heading, []), [])),
+     (sectionN, SOME ((Keyword.document_heading, []), [])),
+     (subsectionN, SOME ((Keyword.document_heading, []), [])),
+     (subsubsectionN, SOME ((Keyword.document_heading, []), [])),
+     (textN, SOME ((Keyword.document_body, []), [])),
+     (txtN, SOME ((Keyword.document_body, []), [])),
+     (text_rawN, SOME ((Keyword.document_raw, []), [])),
      (theoryN, SOME ((Keyword.thy_begin, []), ["theory"])),
      ("ML_file", SOME ((Keyword.thy_load, []), ["ML"]))];
 
 
 (* theory data *)

 val heading =
   (Parse.command headerN ||
     Parse.command chapterN ||
     Parse.command sectionN ||
     Parse.command subsectionN ||
-    Parse.command subsubsectionN) --
+    Parse.command subsubsectionN ||
+    Parse.command textN ||
+    Parse.command txtN ||
+    Parse.command text_rawN) --
   Parse.tags -- Parse.!!! Parse.document_source;
 
 val header =
   (Scan.repeat heading -- Parse.command theoryN -- Parse.tags) |-- Parse.!!! args;