--- a/doc-src/Ref/syntax.tex Tue Jun 19 22:06:08 2012 +0200
+++ b/doc-src/Ref/syntax.tex Wed Jun 20 20:50:04 2012 +0200
@@ -234,101 +234,6 @@
by a slash~({\tt/}) to allow a line break.
\index{ASTs|)}
-
-\section{Translation functions} \label{sec:tr_funs}
-\index{translations|(}
-%
-This section describes the translation function mechanism. By writing \ML{}
-functions, you can do almost everything to terms or \AST{}s during parsing and
-printing. The logic LK is a good example of sophisticated transformations
-between internal and external representations of sequents; here, macros would
-be useless.
-
-A full understanding of translations requires some familiarity
-with Isabelle's internals, especially the datatypes {\tt term}, {\tt typ},
-{\tt Syntax.ast} and the encodings of types and terms as such at the various
-stages of the parsing or printing process. Most users should never need to
-use translation functions.
-
-\subsection{Declaring translation functions}
-There are four kinds of translation functions, with one of these
-coming in two variants. Each such function is associated with a name,
-which triggers calls to it. Such names can be constants (logical or
-syntactic) or type constructors.
-
-Function {\tt print_syntax} displays the sets of names associated with the
-translation functions of a theory under \texttt{parse_ast_translation}, etc.
-You can add new ones via the {\tt ML} section\index{*ML section} of a theory
-definition file. Even though the {\tt ML} section is the very last part of
-the file, newly installed translation functions are already effective when
-processing all of the preceding sections.
-
-The {\tt ML} section's contents are simply copied verbatim near the
-beginning of the \ML\ file generated from a theory definition file.
-Definitions made here are accessible as components of an \ML\
-structure; to make some parts private, use an \ML{} {\tt local}
-declaration. The {\ML} code may install translation functions by
-declaring any of the following identifiers:
-\begin{ttbox}
-val parse_ast_translation : (string * (ast list -> ast)) list
-val print_ast_translation : (string * (ast list -> ast)) list
-val parse_translation : (string * (term list -> term)) list
-val print_translation : (string * (term list -> term)) list
-val typed_print_translation :
- (string * (bool -> typ -> term list -> term)) list
-\end{ttbox}
-
-\subsection{The translation strategy}
-The different kinds of translation functions are called during the
-transformations between parse trees, \AST{}s and terms (recall
-Fig.\ts\ref{fig:parse_print}). Whenever a combination of the form
-$(\mtt"c\mtt"~x@1 \ldots x@n)$ is encountered, and a translation
-function $f$ of appropriate kind exists for $c$, the result is
-computed by the \ML{} function call $f \mtt[ x@1, \ldots, x@n \mtt]$.
-
-For \AST{} translations, the arguments $x@1, \ldots, x@n$ are \AST{}s.
-A combination has the form $\Constant c$ or $\Appl{\Constant c, x@1,
- \ldots, x@n}$. For term translations, the arguments are terms and a
-combination has the form $\ttfct{Const} (c, \tau)$ or $\ttfct{Const}
-(c, \tau) \ttapp x@1 \ttapp \ldots \ttapp x@n$. Terms allow more
-sophisticated transformations than \AST{}s do, typically involving
-abstractions and bound variables. {\em Typed} print translations may
-even peek at the type $\tau$ of the constant they are invoked on; they
-are also passed the current value of the \ttindex{show_sorts} flag.
-
-Regardless of whether they act on terms or \AST{}s, translation
-functions called during the parsing process differ from those for
-printing more fundamentally in their overall behaviour:
-\begin{description}
-\item[Parse translations] are applied bottom-up. The arguments are already in
- translated form. The translations must not fail; exceptions trigger an
- error message. There may never be more than one function associated with
- any syntactic name.
-
-\item[Print translations] are applied top-down. They are supplied with
- arguments that are partly still in internal form. The result again
- undergoes translation; therefore a print translation should not introduce as
- head the very constant that invoked it. The function may raise exception
- \xdx{Match} to indicate failure; in this event it has no effect. Multiple
- functions associated with some syntactic name are tried in an unspecified
- order.
-\end{description}
-
-Only constant atoms --- constructor \ttindex{Constant} for \AST{}s and
-\ttindex{Const} for terms --- can invoke translation functions. This
-causes another difference between parsing and printing.
-
-Parsing starts with a string and the constants are not yet identified.
-Only parse tree heads create {\tt Constant}s in the resulting \AST, as
-described in \S\ref{sec:astofpt}. Macros and parse \AST{} translations may
-introduce further {\tt Constant}s. When the final \AST{} is converted to a
-term, all {\tt Constant}s become {\tt Const}s, as described in
-\S\ref{sec:termofast}.
-
-Printing starts with a well-typed term and all the constants are known. So
-all logical constants and type constructors may invoke print translations.
-These, and macros, may introduce further constants.
-
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "ref"