149 \item @{attribute show_markup} controls direct inlining of markup |
149 \item @{attribute show_markup} controls direct inlining of markup |
150 into the printed representation of formal entities --- notably type |
150 into the printed representation of formal entities --- notably type |
151 and sort constraints. This enables Prover IDE users to retrieve |
151 and sort constraints. This enables Prover IDE users to retrieve |
152 that information via tooltips or popups while hovering with the |
152 that information via tooltips or popups while hovering with the |
153 mouse over the output window, for example. Consequently, this |
153 mouse over the output window, for example. Consequently, this |
154 option is enabled by default for Isabelle/jEdit, but disabled for |
154 option is enabled by default for Isabelle/jEdit. |
155 TTY and Proof~General~/Emacs where document markup would not work. |
|
156 |
155 |
157 \item @{attribute show_types} and @{attribute show_sorts} control |
156 \item @{attribute show_types} and @{attribute show_sorts} control |
158 printing of type constraints for term variables, and sort |
157 printing of type constraints for term variables, and sort |
159 constraints for type variables. By default, neither of these are |
158 constraints for type variables. By default, neither of these are |
160 shown in output. If @{attribute show_sorts} is enabled, types are |
159 shown in output. If @{attribute show_sorts} is enabled, types are |
272 names: it retains the default print mode that certain |
271 names: it retains the default print mode that certain |
273 user-interfaces might have installed for their proper functioning! |
272 user-interfaces might have installed for their proper functioning! |
274 |
273 |
275 \end{description} |
274 \end{description} |
276 |
275 |
277 \begin{warn} |
|
278 The old global reference @{ML print_mode} should never be used |
|
279 directly in applications. Its main reason for being publicly |
|
280 accessible is to support historic versions of Proof~General. |
|
281 \end{warn} |
|
282 |
|
283 \medskip The pretty printer for inner syntax maintains alternative |
276 \medskip The pretty printer for inner syntax maintains alternative |
284 mixfix productions for any print mode name invented by the user, say |
277 mixfix productions for any print mode name invented by the user, say |
285 in commands like @{command notation} or @{command abbreviation}. |
278 in commands like @{command notation} or @{command abbreviation}. |
286 Mode names can be arbitrary, but the following ones have a specific |
279 Mode names can be arbitrary, but the following ones have a specific |
287 meaning by convention: |
280 meaning by convention: |
297 \item @{verbatim internal} dummy print mode that is never active; |
290 \item @{verbatim internal} dummy print mode that is never active; |
298 used internally in Isabelle/Pure. |
291 used internally in Isabelle/Pure. |
299 |
292 |
300 \item @{verbatim xsymbols}: enable proper mathematical symbols |
293 \item @{verbatim xsymbols}: enable proper mathematical symbols |
301 instead of ASCII art.\footnote{This traditional mode name stems from |
294 instead of ASCII art.\footnote{This traditional mode name stems from |
302 the ``X-Symbol'' package for old versions Proof~General with XEmacs, |
295 the ``X-Symbol'' package for classic Proof~General with XEmacs.} |
303 although that package has been superseded by Unicode in recent |
|
304 years.} |
|
305 |
296 |
306 \item @{verbatim HTML}: additional mode that is active in HTML |
297 \item @{verbatim HTML}: additional mode that is active in HTML |
307 presentation of Isabelle theory sources; allows to provide |
298 presentation of Isabelle theory sources; allows to provide |
308 alternative output notation. |
299 alternative output notation. |
309 |
300 |