77 |
77 |
78 *** Document preparation *** |
78 *** Document preparation *** |
79 |
79 |
80 * There is a new short form for antiquotations with a single argument |
80 * There is a new short form for antiquotations with a single argument |
81 that is a cartouche: \<^name>\<open>...\<close> is equivalent to @{name \<open>...\<close>} and |
81 that is a cartouche: \<^name>\<open>...\<close> is equivalent to @{name \<open>...\<close>} and |
82 \<open>...\<close> without control symbol is equivalent to @{cartouche \<open>...\<close>}. The |
82 \<open>...\<close> without control symbol is equivalent to @{cartouche \<open>...\<close>}. |
|
83 \<^name> without following cartouche is equivalent to @{name}. The |
83 standard Isabelle fonts provide glyphs to render important control |
84 standard Isabelle fonts provide glyphs to render important control |
84 symbols, e.g. "\<^verbatim>", "\<^emph>", "\<^bold>". |
85 symbols, e.g. "\<^verbatim>", "\<^emph>", "\<^bold>". |
|
86 |
|
87 * Antiquotations @{noindent}, @{smallskip}, @{medskip}, @{bigskip} with |
|
88 corresponding control symbols \<^noindent>, \<^smallskip>, \<^medskip>, \<^bigskip> specify spacing formally, using |
|
89 standard LaTeX macros of the same names. |
85 |
90 |
86 * System option "document_symbols" determines completion of Isabelle |
91 * System option "document_symbols" determines completion of Isabelle |
87 symbols within document source. |
92 symbols within document source. |
88 |
93 |
89 * Antiquotation @{cartouche} in Isabelle/Pure is the same as @{text}. |
94 * Antiquotation @{cartouche} in Isabelle/Pure is the same as @{text}. |
110 follows: |
115 follows: |
111 |
116 |
112 \<^item> itemize |
117 \<^item> itemize |
113 \<^enum> enumerate |
118 \<^enum> enumerate |
114 \<^descr> description |
119 \<^descr> description |
115 |
|
116 * Text may contain control symbols for markup and formatting as follows: |
|
117 |
|
118 \<^noindent> \noindent |
|
119 \<^smallskip> \smallskip |
|
120 \<^medskip> \medskip |
|
121 \<^bigskip> \bigskip |
|
122 |
120 |
123 * Command 'text_raw' has been clarified: input text is processed as in |
121 * Command 'text_raw' has been clarified: input text is processed as in |
124 'text' (with antiquotations and control symbols). The key difference is |
122 'text' (with antiquotations and control symbols). The key difference is |
125 the lack of the surrounding isabelle markup environment in output. |
123 the lack of the surrounding isabelle markup environment in output. |
126 |
124 |