--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Thu Feb 16 17:09:15 2012 +0100
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Thu Feb 16 22:18:28 2012 +0100
@@ -980,13 +980,10 @@
text {*
\begin{tabular}{rcll}
- @{attribute_def syntax_ambiguity_level} & : & @{text attribute} & default @{text 1} \\
+ @{attribute_def syntax_ambiguity} & : & @{text attribute} & default @{text warning} \\
+ @{attribute_def syntax_ambiguity_limit} & : & @{text attribute} & default @{text 10} \\
\end{tabular}
- \begin{mldecls}
- @{index_ML Syntax.ambiguity_limit: "int Config.T"} \\ %FIXME attribute
- \end{mldecls}
-
Depending on the grammar and the given input, parsing may be
ambiguous. Isabelle lets the Earley parser enumerate all possible
parse trees, and then tries to make the best out of the situation.
@@ -1003,11 +1000,11 @@
\begin{description}
- \item @{attribute syntax_ambiguity_level} determines the number of
- parser results that are tolerated without printing a detailed
- message.
+ \item @{attribute syntax_ambiguity} determines reaction on multiple
+ results of parsing; this string option can be set to @{text
+ "ignore"}, @{text "warning"}, or @{text "error"}.
- \item @{ML Syntax.ambiguity_limit} determines the number of
+ \item @{attribute syntax_ambiguity_limit} determines the number of
resulting parse trees that are shown as part of the printed message
in case of an ambiguity.