24 \begin{matharray}{rcl} |
24 \begin{matharray}{rcl} |
25 @{command_def "chapter"} & : & @{text "any \<rightarrow> any"} \\ |
25 @{command_def "chapter"} & : & @{text "any \<rightarrow> any"} \\ |
26 @{command_def "section"} & : & @{text "any \<rightarrow> any"} \\ |
26 @{command_def "section"} & : & @{text "any \<rightarrow> any"} \\ |
27 @{command_def "subsection"} & : & @{text "any \<rightarrow> any"} \\ |
27 @{command_def "subsection"} & : & @{text "any \<rightarrow> any"} \\ |
28 @{command_def "subsubsection"} & : & @{text "any \<rightarrow> any"} \\ |
28 @{command_def "subsubsection"} & : & @{text "any \<rightarrow> any"} \\ |
|
29 @{command_def "paragraph"} & : & @{text "any \<rightarrow> any"} \\ |
|
30 @{command_def "subparagraph"} & : & @{text "any \<rightarrow> any"} \\ |
29 @{command_def "text"} & : & @{text "any \<rightarrow> any"} \\ |
31 @{command_def "text"} & : & @{text "any \<rightarrow> any"} \\ |
30 @{command_def "txt"} & : & @{text "any \<rightarrow> any"} \\ |
32 @{command_def "txt"} & : & @{text "any \<rightarrow> any"} \\ |
31 @{command_def "text_raw"} & : & @{text "any \<rightarrow> any"} \\ |
33 @{command_def "text_raw"} & : & @{text "any \<rightarrow> any"} \\ |
32 \end{matharray} |
34 \end{matharray} |
33 |
35 |
42 markup commands, but have a different status within Isabelle/Isar |
44 markup commands, but have a different status within Isabelle/Isar |
43 syntax. |
45 syntax. |
44 |
46 |
45 @{rail \<open> |
47 @{rail \<open> |
46 (@@{command chapter} | @@{command section} | @@{command subsection} | |
48 (@@{command chapter} | @@{command section} | @@{command subsection} | |
47 @@{command subsubsection} | @@{command text} | @@{command txt}) @{syntax text} |
49 @@{command subsubsection} | @@{command paragraph} | @@{command subparagraph} | |
48 ; |
50 @@{command text} | @@{command txt} | @@{command text_raw}) @{syntax text} |
49 @@{command text_raw} @{syntax text} |
51 \<close>} |
50 \<close>} |
52 |
51 |
53 \<^descr> @{command chapter}, @{command section}, @{command subsection} etc.\ mark |
52 \<^descr> @{command chapter}, @{command section}, @{command subsection}, and |
54 section headings within the theory source. This works in any context, even |
53 @{command subsubsection} mark chapter and section headings within the |
55 before the initial @{command theory} command. The corresponding {\LaTeX} |
54 theory source; this works in any context, even before the initial |
56 macros are @{verbatim \<open>\isamarkupchapter\<close>}, @{verbatim |
55 @{command theory} command. The corresponding {\LaTeX} macros are |
57 \<open>\isamarkupsection\<close>}, @{verbatim \<open>\isamarkupsubsection\<close>} etc.\ |
56 @{verbatim \<open>\isamarkupchapter\<close>}, @{verbatim \<open>\isamarkupsection\<close>}, |
|
57 @{verbatim \<open>\isamarkupsubsection\<close>}, @{verbatim \<open>\isamarkupsubsubsection\<close>}. |
|
58 |
58 |
59 \<^descr> @{command text} and @{command txt} specify paragraphs of plain text. |
59 \<^descr> @{command text} and @{command txt} specify paragraphs of plain text. |
60 This corresponds to a {\LaTeX} environment @{verbatim |
60 This corresponds to a {\LaTeX} environment @{verbatim |
61 \<open>\begin{isamarkuptext}\<close>} @{text "\<dots>"} @{verbatim \<open>\end{isamarkuptext}\<close>} |
61 \<open>\begin{isamarkuptext}\<close>} @{text "\<dots>"} @{verbatim \<open>\end{isamarkuptext}\<close>} |
62 etc. |
62 etc. |
63 |
63 |
64 \<^descr> @{command text_raw} inserts {\LaTeX} source directly into the |
64 \<^descr> @{command text_raw} is similar to @{command text}, but without |
65 output, without additional markup. Thus the full range of document |
65 any surrounding markup environment. This allows to inject arbitrary |
66 manipulations becomes available, at the risk of messing up document |
66 {\LaTeX} source into the generated document. |
67 output. |
67 |
68 |
68 |
69 |
69 All text passed to any of the above markup commands may refer to formal |
70 Except for @{command "text_raw"}, the text passed to any of the above |
70 entities via \emph{document antiquotations}, see also \secref{sec:antiq}. |
71 markup commands may refer to formal entities via \emph{document |
71 These are interpreted in the present theory or proof context. |
72 antiquotations}, see also \secref{sec:antiq}. These are interpreted in the |
|
73 present theory or proof context. |
|
74 |
72 |
75 \<^medskip> |
73 \<^medskip> |
76 The proof markup commands closely resemble those for theory |
74 The proof markup commands closely resemble those for theory |
77 specifications, but have a different formal status and produce |
75 specifications, but have a different formal status and produce |
78 different {\LaTeX} macros. |
76 different {\LaTeX} macros. |