--- a/doc-src/Ref/defining.tex Wed Jun 09 15:00:32 2004 +0200
+++ b/doc-src/Ref/defining.tex Wed Jun 09 18:50:38 2004 +0200
@@ -494,25 +494,6 @@
"-" :: exp => exp ("- _" [3] 3)
end
\end{ttbox}
-If you put this into a file {\tt ExpSyntax.thy} and load it by {\tt
- use_thy"ExpSyntax"}, you can run some tests:
-\begin{ttbox}
-val read_exp = Syntax.test_read (syn_of ExpSyntax.thy) "exp";
-{\out val it = fn : string -> unit}
-read_exp "0 * 0 * 0 * 0 + 0 + 0 + 0";
-{\out tokens: "0" "*" "0" "*" "0" "*" "0" "+" "0" "+" "0" "+" "0"}
-{\out raw: ("+" ("+" ("+" ("*" "0" ("*" "0" ("*" "0" "0"))) "0") "0") "0")}
-{\out \vdots}
-read_exp "0 + - 0 + 0";
-{\out tokens: "0" "+" "-" "0" "+" "0"}
-{\out raw: ("+" ("+" "0" ("-" "0")) "0")}
-{\out \vdots}
-\end{ttbox}
-The output of \ttindex{Syntax.test_read} includes the token list ({\tt
- tokens}) and the raw \AST{} directly derived from the parse tree,
-ignoring parse \AST{} translations. The rest is tracing information
-provided by the macro expander (see \S\ref{sec:macros}).
-
Executing {\tt Syntax.print_gram} reveals the productions derived from the
above mixfix declarations (lots of additional information deleted):
\begin{ttbox}
--- a/doc-src/Ref/syntax.tex Wed Jun 09 15:00:32 2004 +0200
+++ b/doc-src/Ref/syntax.tex Wed Jun 09 18:50:38 2004 +0200
@@ -551,15 +551,13 @@
The term \verb|%Nil.t| will be printed as \verb|%[].t|, which might not be
expected! Guess how type~{\tt Nil} is printed?
-Normalizing an \AST{} involves repeatedly applying macro rules until
-none are applicable. Macro rules are chosen in order of appearance in
-the theory definitions. You can watch the normalization of \AST{}s
-during parsing and printing by setting \ttindex{Syntax.trace_ast}
-to {\tt true}.\index{tracing!of macros} Alternatively, use
-\ttindex{Syntax.test_read}. The information displayed when tracing
-includes the \AST{} before normalization ({\tt pre}), redexes with
-results ({\tt rewrote}), the normal form finally reached ({\tt post})
-and some statistics ({\tt normalize}).
+Normalizing an \AST{} involves repeatedly applying macro rules until none are
+applicable. Macro rules are chosen in order of appearance in the theory
+definitions. You can watch the normalization of \AST{}s during parsing and
+printing by setting \ttindex{Syntax.trace_ast} to {\tt true}.\index{tracing!of
+ macros} The information displayed when tracing includes the \AST{} before
+normalization ({\tt pre}), redexes with results ({\tt rewrote}), the normal
+form finally reached ({\tt post}) and some statistics ({\tt normalize}).
\subsection{Example: the syntax of finite sets}
\index{examples!of macros}