explicit tag for document commands: avoid implicit use of document_tags;
authorwenzelm
Tue Dec 05 15:55:14 2017 +0100 (12 months ago)
changeset 671398fe0aba577af
parent 67138 82283d52b4d6
child 67140 386a31d6d17a
explicit tag for document commands: avoid implicit use of document_tags;
lib/texinputs/isabelle.sty
src/Doc/Isar_Ref/Document_Preparation.thy
src/Doc/System/Presentation.thy
src/Pure/Isar/keyword.ML
src/Pure/Thy/thy_header.ML
     1.1 --- a/lib/texinputs/isabelle.sty	Tue Dec 05 15:29:37 2017 +0100
     1.2 +++ b/lib/texinputs/isabelle.sty	Tue Dec 05 15:55:14 2017 +0100
     1.3 @@ -250,6 +250,7 @@
     1.4  \newcommand{\isafoldtag}[1]%
     1.5  {\includecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{\isafold{#1}}}
     1.6  
     1.7 +\isakeeptag{document}
     1.8  \isakeeptag{theory}
     1.9  \isakeeptag{proof}
    1.10  \isakeeptag{ML}
     2.1 --- a/src/Doc/Isar_Ref/Document_Preparation.thy	Tue Dec 05 15:29:37 2017 +0100
     2.2 +++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Tue Dec 05 15:55:14 2017 +0100
     2.3 @@ -473,6 +473,7 @@
     2.4  
     2.5    \<^medskip>
     2.6    \begin{tabular}{ll}
     2.7 +    \<open>document\<close> & document markup commands \\
     2.8      \<open>theory\<close> & theory begin/end \\
     2.9      \<open>proof\<close> & all proof commands \\
    2.10      \<open>ML\<close> & all commands involving ML code \\
     3.1 --- a/src/Doc/System/Presentation.thy	Tue Dec 05 15:29:37 2017 +0100
     3.2 +++ b/src/Doc/System/Presentation.thy	Tue Dec 05 15:55:14 2017 +0100
     3.3 @@ -182,7 +182,7 @@
     3.4    pairs: ``\<^verbatim>\<open>+\<close>\<open>foo\<close>'' (or just ``\<open>foo\<close>'') means to keep, ``\<^verbatim>\<open>-\<close>\<open>foo\<close>'' to
     3.5    drop, and ``\<^verbatim>\<open>/\<close>\<open>foo\<close>'' to fold text tagged as \<open>foo\<close>. The builtin default is
     3.6    equivalent to the tag specification
     3.7 -  ``\<^verbatim>\<open>+theory,+proof,+ML,+visible,-invisible\<close>''; see also the {\LaTeX} macros
     3.8 +  ``\<^verbatim>\<open>+document,+theory,+proof,+ML,+visible,-invisible\<close>''; see also the {\LaTeX} macros
     3.9    \<^verbatim>\<open>\isakeeptag\<close>, \<^verbatim>\<open>\isadroptag\<close>, and \<^verbatim>\<open>\isafoldtag\<close>, in
    3.10    \<^file>\<open>~~/lib/texinputs/isabelle.sty\<close>.
    3.11  
     4.1 --- a/src/Pure/Isar/keyword.ML	Tue Dec 05 15:29:37 2017 +0100
     4.2 +++ b/src/Pure/Isar/keyword.ML	Tue Dec 05 15:55:14 2017 +0100
     4.3 @@ -38,6 +38,8 @@
     4.4    val no_spec: spec
     4.5    val before_command_spec: spec
     4.6    val quasi_command_spec: spec
     4.7 +  val document_heading_spec: spec
     4.8 +  val document_body_spec: spec
     4.9    type keywords
    4.10    val minor_keywords: keywords -> Scan.lexicon
    4.11    val major_keywords: keywords -> Scan.lexicon
    4.12 @@ -127,6 +129,8 @@
    4.13  val no_spec: spec = (("", []), []);
    4.14  val before_command_spec: spec = ((before_command, []), []);
    4.15  val quasi_command_spec: spec = ((quasi_command, []), []);
    4.16 +val document_heading_spec: spec = (("document_heading", []), ["document"]);
    4.17 +val document_body_spec: spec = (("document_body", []), ["document"]);
    4.18  
    4.19  type entry =
    4.20   {pos: Position.T,
     5.1 --- a/src/Pure/Thy/thy_header.ML	Tue Dec 05 15:29:37 2017 +0100
     5.2 +++ b/src/Pure/Thy/thy_header.ML	Tue Dec 05 15:55:14 2017 +0100
     5.3 @@ -77,15 +77,15 @@
     5.4       ((importsN, \<^here>), Keyword.quasi_command_spec),
     5.5       ((keywordsN, \<^here>), Keyword.quasi_command_spec),
     5.6       ((abbrevsN, \<^here>), Keyword.quasi_command_spec),
     5.7 -     ((chapterN, \<^here>), ((Keyword.document_heading, []), [])),
     5.8 -     ((sectionN, \<^here>), ((Keyword.document_heading, []), [])),
     5.9 -     ((subsectionN, \<^here>), ((Keyword.document_heading, []), [])),
    5.10 -     ((subsubsectionN, \<^here>), ((Keyword.document_heading, []), [])),
    5.11 -     ((paragraphN, \<^here>), ((Keyword.document_heading, []), [])),
    5.12 -     ((subparagraphN, \<^here>), ((Keyword.document_heading, []), [])),
    5.13 -     ((textN, \<^here>), ((Keyword.document_body, []), [])),
    5.14 -     ((txtN, \<^here>), ((Keyword.document_body, []), [])),
    5.15 -     ((text_rawN, \<^here>), ((Keyword.document_raw, []), [])),
    5.16 +     ((chapterN, \<^here>), Keyword.document_heading_spec),
    5.17 +     ((sectionN, \<^here>), Keyword.document_heading_spec),
    5.18 +     ((subsectionN, \<^here>), Keyword.document_heading_spec),
    5.19 +     ((subsubsectionN, \<^here>), Keyword.document_heading_spec),
    5.20 +     ((paragraphN, \<^here>), Keyword.document_heading_spec),
    5.21 +     ((subparagraphN, \<^here>), Keyword.document_heading_spec),
    5.22 +     ((textN, \<^here>), Keyword.document_body_spec),
    5.23 +     ((txtN, \<^here>), Keyword.document_body_spec),
    5.24 +     ((text_rawN, \<^here>), ((Keyword.document_raw, []), ["document"])),
    5.25       ((theoryN, \<^here>), ((Keyword.thy_begin, []), ["theory"])),
    5.26       (("ML", \<^here>), ((Keyword.thy_decl, []), ["ML"]))];
    5.27