# HG changeset patch
# User wenzelm
# Date 1086799838 -7200
# Node ID 55e83c32cdecf7d3991fa557c1a5138a3c4ff13c
# Parent  659707452f55b636232e68dd3ce817112ee9d86f
removed Syntax.test_read;

diff -r 659707452f55 -r 55e83c32cdec doc-src/Ref/defining.tex
--- 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}
diff -r 659707452f55 -r 55e83c32cdec doc-src/Ref/syntax.tex
--- 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}