# HG changeset patch # User wenzelm # Date 1328214101 -3600 # Node ID 6233d0b74d71b5829686c1a4e232728f091c54f9 # Parent d90a650a5fb90e76ab90aee018fd737f67c3c7e7 updated section on print modes; diff -r d90a650a5fb9 -r 6233d0b74d71 doc-src/IsarRef/Thy/Inner_Syntax.thy --- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Thu Feb 02 20:26:44 2012 +0100 +++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Thu Feb 02 21:21:41 2012 +0100 @@ -32,7 +32,7 @@ section {* Printing logical entities *} -subsection {* Diagnostic commands *} +subsection {* Diagnostic commands \label{sec:print-diag} *} text {* \begin{matharray}{rcl} @@ -104,11 +104,11 @@ All of the diagnostic commands above admit a list of @{text modes} to be specified, which is appended to the current print mode; see - \secref{sec:print-modes}. Thus the output behavior may be modified - according particular print mode features. For example, @{command - "pr"}~@{text "(latex xsymbols)"} would print the current proof state - with mathematical symbols and special characters represented in - {\LaTeX} source, according to the Isabelle style + also \secref{sec:print-modes}. Thus the output behavior may be + modified according particular print mode features. For example, + @{command "pr"}~@{text "(latex xsymbols)"} would print the current + proof state with mathematical symbols and special characters + represented in {\LaTeX} source, according to the Isabelle style \cite{isabelle-sys}. Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more @@ -232,6 +232,77 @@ *} +subsection {* Alternative print modes \label{sec:print-modes} *} + +text {* + \begin{mldecls} + @{index_ML print_mode_value: "unit -> string list"} \\ + @{index_ML Print_Mode.with_modes: "string list -> ('a -> 'b) -> 'a -> 'b"} \\ + \end{mldecls} + + The \emph{print mode} facility allows to modify various operations + for printing. Commands like @{command typ}, @{command term}, + @{command thm} (see \secref{sec:print-diag}) take additional print + modes as optional argument. The underlying ML operations are as + follows. + + \begin{description} + + \item @{ML "print_mode_value ()"} yields the list of currently + active print mode names. This should be understood as symbolic + representation of certain individual features for printing (with + precedence from left to right). + + \item @{ML Print_Mode.with_modes}~@{text "modes f x"} evaluates + @{text "f x"} in an execution context where the print mode is + prepended by the given @{text "modes"}. This provides a thread-safe + way to augment print modes. It is also monotonic in the set of mode + names: it retains the default print mode that certain + user-interfaces might have installed for their proper functioning! + + \end{description} + + \begin{warn} + The old global reference @{ML print_mode} should never be used + directly in applications. Its main reason for being publicly + accessible is to support historic versions of Proof~General. + \end{warn} + + \medskip The pretty printer for inner syntax maintains alternative + mixfix productions for any print mode name invented by the user, say + in commands like @{command notation} or @{command abbreviation}. + Mode names can be arbitrary, but the following ones have a specific + meaning by convention: + + \begin{itemize} + + \item @{verbatim "\"\""} (the empty string): default mode; + implicitly active as last element in the list of modes. + + \item @{verbatim input}: dummy print mode that is never active; may + be used to specify notation that is only available for input. + + \item @{verbatim internal} dummy print mode that is never active; + used internally in Isabelle/Pure. + + \item @{verbatim xsymbols}: enable proper mathematical symbols + instead of ASCII art.\footnote{This traditional mode name stems from + the ``X-Symbol'' package for old versions Proof~General with XEmacs, + although that package has been superseded by Unicode in recent + years.} + + \item @{verbatim HTML}: additional mode that is active in HTML + presentation of Isabelle theory sources; allows to provide + alternative output notation. + + \item @{verbatim latex}: additional mode that is active in {\LaTeX} + document preparation of Isabelle theory sources; allows to provide + alternative output notation. + + \end{itemize} +*} + + subsection {* Printing limits *} text {* diff -r d90a650a5fb9 -r 6233d0b74d71 doc-src/IsarRef/Thy/document/Inner_Syntax.tex --- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Thu Feb 02 20:26:44 2012 +0100 +++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Thu Feb 02 21:21:41 2012 +0100 @@ -50,7 +50,7 @@ } \isamarkuptrue% % -\isamarkupsubsection{Diagnostic commands% +\isamarkupsubsection{Diagnostic commands \label{sec:print-diag}% } \isamarkuptrue% % @@ -176,10 +176,11 @@ All of the diagnostic commands above admit a list of \isa{modes} to be specified, which is appended to the current print mode; see - \secref{sec:print-modes}. Thus the output behavior may be modified - according particular print mode features. For example, \hyperlink{command.pr}{\mbox{\isa{\isacommand{pr}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}latex\ xsymbols{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} would print the current proof state - with mathematical symbols and special characters represented in - {\LaTeX} source, according to the Isabelle style + also \secref{sec:print-modes}. Thus the output behavior may be + modified according particular print mode features. For example, + \hyperlink{command.pr}{\mbox{\isa{\isacommand{pr}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}latex\ xsymbols{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} would print the current + proof state with mathematical symbols and special characters + represented in {\LaTeX} source, according to the Isabelle style \cite{isabelle-sys}. Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more @@ -301,6 +302,79 @@ \end{isamarkuptext}% \isamarkuptrue% % +\isamarkupsubsection{Alternative print modes \label{sec:print-modes}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\begin{mldecls} + \indexdef{}{ML}{print\_mode\_value}\verb|print_mode_value: unit -> string list| \\ + \indexdef{}{ML}{Print\_Mode.with\_modes}\verb|Print_Mode.with_modes: string list -> ('a -> 'b) -> 'a -> 'b| \\ + \end{mldecls} + + The \emph{print mode} facility allows to modify various operations + for printing. Commands like \hyperlink{command.typ}{\mbox{\isa{\isacommand{typ}}}}, \hyperlink{command.term}{\mbox{\isa{\isacommand{term}}}}, + \hyperlink{command.thm}{\mbox{\isa{\isacommand{thm}}}} (see \secref{sec:print-diag}) take additional print + modes as optional argument. The underlying ML operations are as + follows. + + \begin{description} + + \item \verb|print_mode_value ()| yields the list of currently + active print mode names. This should be understood as symbolic + representation of certain individual features for printing (with + precedence from left to right). + + \item \verb|Print_Mode.with_modes|~\isa{{\isaliteral{22}{\isachardoublequote}}modes\ f\ x{\isaliteral{22}{\isachardoublequote}}} evaluates + \isa{{\isaliteral{22}{\isachardoublequote}}f\ x{\isaliteral{22}{\isachardoublequote}}} in an execution context where the print mode is + prepended by the given \isa{{\isaliteral{22}{\isachardoublequote}}modes{\isaliteral{22}{\isachardoublequote}}}. This provides a thread-safe + way to augment print modes. It is also monotonic in the set of mode + names: it retains the default print mode that certain + user-interfaces might have installed for their proper functioning! + + \end{description} + + \begin{warn} + The old global reference \verb|print_mode| should never be used + directly in applications. Its main reason for being publicly + accessible is to support historic versions of Proof~General. + \end{warn} + + \medskip The pretty printer for inner syntax maintains alternative + mixfix productions for any print mode name invented by the user, say + in commands like \hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}} or \hyperlink{command.abbreviation}{\mbox{\isa{\isacommand{abbreviation}}}}. + Mode names can be arbitrary, but the following ones have a specific + meaning by convention: + + \begin{itemize} + + \item \verb|""| (the empty string): default mode; + implicitly active as last element in the list of modes. + + \item \verb|input|: dummy print mode that is never active; may + be used to specify notation that is only available for input. + + \item \verb|internal| dummy print mode that is never active; + used internally in Isabelle/Pure. + + \item \verb|xsymbols|: enable proper mathematical symbols + instead of ASCII art.\footnote{This traditional mode name stems from + the ``X-Symbol'' package for old versions Proof~General with XEmacs, + although that package has been superseded by Unicode in recent + years.} + + \item \verb|HTML|: additional mode that is active in HTML + presentation of Isabelle theory sources; allows to provide + alternative output notation. + + \item \verb|latex|: additional mode that is active in {\LaTeX} + document preparation of Isabelle theory sources; allows to provide + alternative output notation. + + \end{itemize}% +\end{isamarkuptext}% +\isamarkuptrue% +% \isamarkupsubsection{Printing limits% } \isamarkuptrue% diff -r d90a650a5fb9 -r 6233d0b74d71 doc-src/Ref/defining.tex --- a/doc-src/Ref/defining.tex Thu Feb 02 20:26:44 2012 +0100 +++ b/doc-src/Ref/defining.tex Thu Feb 02 21:21:41 2012 +0100 @@ -224,43 +224,6 @@ \index{mixfix declarations|)} -\section{*Alternative print modes} \label{sec:prmodes} -\index{print modes|(} -% -Isabelle's pretty printer supports alternative output syntaxes. These -may be used independently or in cooperation. The currently active -print modes (with precedence from left to right) are determined by a -reference variable. -\begin{ttbox}\index{*print_mode} -print_mode: string list ref -\end{ttbox} -Initially this may already contain some print mode identifiers, -depending on how Isabelle has been invoked (e.g.\ by some user -interface). So changes should be incremental --- adding or deleting -modes relative to the current value. - -Any \ML{} string is a legal print mode identifier, without any predeclaration -required. The following names should be considered reserved, though: -\texttt{""} (the empty string), \texttt{symbols}, \texttt{xsymbols}, and -\texttt{latex}. - -There is a separate table of mixfix productions for pretty printing -associated with each print mode. The currently active ones are -conceptually just concatenated from left to right, with the standard -syntax output table always coming last as default. Thus mixfix -productions of preceding modes in the list may override those of later -ones. - -\medskip The canonical application of print modes is optional printing -of mathematical symbols from a special screen font instead of {\sc - ascii}. Another example is to re-use Isabelle's advanced -$\lambda$-term printing mechanisms to generate completely different -output, say for interfacing external tools like \rmindex{model - checkers} (see also \texttt{HOL/Modelcheck}). - -\index{print modes|)} - - \section{Ambiguity of parsed expressions} \label{sec:ambiguity} \index{ambiguity!of parsed expressions}