--- a/doc-src/Ref/syntax.tex Fri Jun 22 15:03:41 2012 +0200
+++ b/doc-src/Ref/syntax.tex Mon Jun 18 16:30:20 2012 +0200
@@ -8,49 +8,9 @@
\newcommand\Appl[1]{\ttfct{Appl}\,[#1]}
\index{syntax!transformations|(}
-This chapter is intended for experienced Isabelle users who need to define
-macros or code their own translation functions. It describes the
-transformations between parse trees, abstract syntax trees and terms.
-
-
\section{Abstract syntax trees} \label{sec:asts}
\index{ASTs|(}
-The parser, given a token list from the lexer, applies productions to yield
-a parse tree\index{parse trees}. By applying some internal transformations
-the parse tree becomes an abstract syntax tree, or \AST{}. Macro
-expansion, further translations and finally type inference yields a
-well-typed term. The printing process is the reverse, except for some
-subtleties to be discussed later.
-
-Figure~\ref{fig:parse_print} outlines the parsing and printing process.
-Much of the complexity is due to the macro mechanism. Using macros, you
-can specify most forms of concrete syntax without writing any \ML{} code.
-
-\begin{figure}
-\begin{center}
-\begin{tabular}{cl}
-string & \\
-$\downarrow$ & lexer, parser \\
-parse tree & \\
-$\downarrow$ & parse \AST{} translation \\
-\AST{} & \\
-$\downarrow$ & \AST{} rewriting (macros) \\
-\AST{} & \\
-$\downarrow$ & parse translation, type inference \\
---- well-typed term --- & \\
-$\downarrow$ & print translation \\
-\AST{} & \\
-$\downarrow$ & \AST{} rewriting (macros) \\
-\AST{} & \\
-$\downarrow$ & print \AST{} translation \\
-string &
-\end{tabular}
-
-\end{center}
-\caption{Parsing and printing}\label{fig:parse_print}
-\end{figure}
-
Abstract syntax trees are an intermediate form between the raw parse trees
and the typed $\lambda$-terms. An \AST{} is either an atom (constant or
variable) or a list of {\em at least two\/} subtrees. Internally, they