
diff -r e21f4d5b9636 -r 8537313dd261 doc-src/Ref/syntax.tex
--- 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"




