--- 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 {*
--- 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%
--- 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}