explicit tag for document commands: avoid implicit use of document_tags;

--- a/lib/texinputs/isabelle.sty	Tue Dec 05 15:29:37 2017 +0100
+++ b/lib/texinputs/isabelle.sty	Tue Dec 05 15:55:14 2017 +0100
@@ -250,6 +250,7 @@
 \newcommand{\isafoldtag}[1]%
 {\includecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{\isafold{#1}}}
 
+\isakeeptag{document}
 \isakeeptag{theory}
 \isakeeptag{proof}
 \isakeeptag{ML}

--- a/src/Doc/Isar_Ref/Document_Preparation.thy	Tue Dec 05 15:29:37 2017 +0100
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Tue Dec 05 15:55:14 2017 +0100
@@ -473,6 +473,7 @@
 
   \<^medskip>
   \begin{tabular}{ll}
+    \<open>document\<close> & document markup commands \\
     \<open>theory\<close> & theory begin/end \\
     \<open>proof\<close> & all proof commands \\
     \<open>ML\<close> & all commands involving ML code \\

--- a/src/Doc/System/Presentation.thy	Tue Dec 05 15:29:37 2017 +0100
+++ b/src/Doc/System/Presentation.thy	Tue Dec 05 15:55:14 2017 +0100
@@ -182,7 +182,7 @@
   pairs: ``\<^verbatim>\<open>+\<close>\<open>foo\<close>'' (or just ``\<open>foo\<close>'') means to keep, ``\<^verbatim>\<open>-\<close>\<open>foo\<close>'' to
   drop, and ``\<^verbatim>\<open>/\<close>\<open>foo\<close>'' to fold text tagged as \<open>foo\<close>. The builtin default is
   equivalent to the tag specification
-  ``\<^verbatim>\<open>+theory,+proof,+ML,+visible,-invisible\<close>''; see also the {\LaTeX} macros
+  ``\<^verbatim>\<open>+document,+theory,+proof,+ML,+visible,-invisible\<close>''; see also the {\LaTeX} macros
   \<^verbatim>\<open>\isakeeptag\<close>, \<^verbatim>\<open>\isadroptag\<close>, and \<^verbatim>\<open>\isafoldtag\<close>, in
   \<^file>\<open>~~/lib/texinputs/isabelle.sty\<close>.
 

--- a/src/Pure/Isar/keyword.ML	Tue Dec 05 15:29:37 2017 +0100
+++ b/src/Pure/Isar/keyword.ML	Tue Dec 05 15:55:14 2017 +0100
@@ -38,6 +38,8 @@
   val no_spec: spec
   val before_command_spec: spec
   val quasi_command_spec: spec
+  val document_heading_spec: spec
+  val document_body_spec: spec
   type keywords
   val minor_keywords: keywords -> Scan.lexicon
   val major_keywords: keywords -> Scan.lexicon
@@ -127,6 +129,8 @@
 val no_spec: spec = (("", []), []);
 val before_command_spec: spec = ((before_command, []), []);
 val quasi_command_spec: spec = ((quasi_command, []), []);
+val document_heading_spec: spec = (("document_heading", []), ["document"]);
+val document_body_spec: spec = (("document_body", []), ["document"]);
 
 type entry =
  {pos: Position.T,

--- a/src/Pure/Thy/thy_header.ML	Tue Dec 05 15:29:37 2017 +0100
+++ b/src/Pure/Thy/thy_header.ML	Tue Dec 05 15:55:14 2017 +0100
@@ -77,15 +77,15 @@
      ((importsN, \<^here>), Keyword.quasi_command_spec),
      ((keywordsN, \<^here>), Keyword.quasi_command_spec),
      ((abbrevsN, \<^here>), Keyword.quasi_command_spec),
-     ((chapterN, \<^here>), ((Keyword.document_heading, []), [])),
-     ((sectionN, \<^here>), ((Keyword.document_heading, []), [])),
-     ((subsectionN, \<^here>), ((Keyword.document_heading, []), [])),
-     ((subsubsectionN, \<^here>), ((Keyword.document_heading, []), [])),
-     ((paragraphN, \<^here>), ((Keyword.document_heading, []), [])),
-     ((subparagraphN, \<^here>), ((Keyword.document_heading, []), [])),
-     ((textN, \<^here>), ((Keyword.document_body, []), [])),
-     ((txtN, \<^here>), ((Keyword.document_body, []), [])),
-     ((text_rawN, \<^here>), ((Keyword.document_raw, []), [])),
+     ((chapterN, \<^here>), Keyword.document_heading_spec),
+     ((sectionN, \<^here>), Keyword.document_heading_spec),
+     ((subsectionN, \<^here>), Keyword.document_heading_spec),
+     ((subsubsectionN, \<^here>), Keyword.document_heading_spec),
+     ((paragraphN, \<^here>), Keyword.document_heading_spec),
+     ((subparagraphN, \<^here>), Keyword.document_heading_spec),
+     ((textN, \<^here>), Keyword.document_body_spec),
+     ((txtN, \<^here>), Keyword.document_body_spec),
+     ((text_rawN, \<^here>), ((Keyword.document_raw, []), ["document"])),
      ((theoryN, \<^here>), ((Keyword.thy_begin, []), ["theory"])),
      (("ML", \<^here>), ((Keyword.thy_decl, []), ["ML"]))];