99 |
99 |
100 \<^descr> @{command "print_state"} prints the current proof state (if |
100 \<^descr> @{command "print_state"} prints the current proof state (if |
101 present), including current facts and goals. |
101 present), including current facts and goals. |
102 |
102 |
103 |
103 |
104 All of the diagnostic commands above admit a list of \<open>modes\<close> |
104 All of the diagnostic commands above admit a list of \<open>modes\<close> to be |
105 to be specified, which is appended to the current print mode; see |
105 specified, which is appended to the current print mode; see also |
106 also \secref{sec:print-modes}. Thus the output behavior may be |
106 \secref{sec:print-modes}. Thus the output behavior may be modified according |
107 modified according particular print mode features. For example, |
107 particular print mode features. For example, @{command |
108 @{command "print_state"}~\<open>(latex xsymbols)\<close> prints the |
108 "print_state"}~\<open>(latex)\<close> prints the current proof state with mathematical |
109 current proof state with mathematical symbols and special characters |
109 symbols and special characters represented in {\LaTeX} source, according to |
110 represented in {\LaTeX} source, according to the Isabelle style |
110 the Isabelle style @{cite "isabelle-system"}. |
111 @{cite "isabelle-system"}. |
|
112 |
111 |
113 Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more |
112 Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more |
114 systematic way to include formal items into the printed text |
113 systematic way to include formal items into the printed text |
115 document. |
114 document. |
116 \<close> |
115 \<close> |
276 be used to specify notation that is only available for input. |
275 be used to specify notation that is only available for input. |
277 |
276 |
278 \<^item> \<^verbatim>\<open>internal\<close> dummy print mode that is never active; |
277 \<^item> \<^verbatim>\<open>internal\<close> dummy print mode that is never active; |
279 used internally in Isabelle/Pure. |
278 used internally in Isabelle/Pure. |
280 |
279 |
281 \<^item> \<^verbatim>\<open>xsymbols\<close>: enable proper mathematical symbols |
280 \<^item> \<^verbatim>\<open>ASCII\<close>: prefer ASCII art over mathematical symbols. |
282 instead of ASCII art.\<^footnote>\<open>This traditional mode name stems from |
|
283 the ``X-Symbol'' package for classic Proof~General with XEmacs.\<close> |
|
284 |
281 |
285 \<^item> \<^verbatim>\<open>latex\<close>: additional mode that is active in {\LaTeX} |
282 \<^item> \<^verbatim>\<open>latex\<close>: additional mode that is active in {\LaTeX} |
286 document preparation of Isabelle theory sources; allows to provide |
283 document preparation of Isabelle theory sources; allows to provide |
287 alternative output notation. |
284 alternative output notation. |
288 \<close> |
285 \<close> |