--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Sat Feb 04 18:33:04 2012 +0100
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Sun Feb 05 18:11:19 2012 +0100
@@ -974,6 +974,45 @@
*}
+subsection {* Ambiguity of parsed expressions *}
+
+text {*
+ \begin{tabular}{rcll}
+ @{attribute_def syntax_ambiguity_level} & : & @{text attribute} & default @{text 1} \\
+ \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.
+ Terms that cannot be type-checked are filtered out, which often
+ leads to a unique result in the end. Unlike regular type
+ reconstruction, which is applied to the whole collection of input
+ terms simultaneously, the filtering stage only treats each given
+ term in isolation. Filtering is also not attempted for individual
+ types or raw ASTs (as required for @{command translations}).
+
+ Certain warning or error messages are printed, depending on the
+ situation and the given configuration options. Parsing ultimately
+ fails, if multiple results remain after the filtering phase.
+
+ \begin{description}
+
+ \item @{attribute syntax_ambiguity_level} determines the number of
+ parser results that are tolerated without printing a detailed
+ message.
+
+ \item @{ML Syntax.ambiguity_limit} determines the number of
+ resulting parse trees that are shown as part of the printed message
+ in case of an ambiguity.
+
+ \end{description}
+*}
+
+
section {* Raw syntax and translations \label{sec:syn-trans} *}
text {*
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Sat Feb 04 18:33:04 2012 +0100
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Sun Feb 05 18:11:19 2012 +0100
@@ -1147,6 +1147,47 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isamarkupsubsection{Ambiguity of parsed expressions%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{tabular}{rcll}
+ \indexdef{}{attribute}{syntax\_ambiguity\_level}\hypertarget{attribute.syntax-ambiguity-level}{\hyperlink{attribute.syntax-ambiguity-level}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}ambiguity{\isaliteral{5F}{\isacharunderscore}}level}}}} & : & \isa{attribute} & default \isa{{\isadigit{1}}} \\
+ \end{tabular}
+
+ \begin{mldecls}
+ \indexdef{}{ML}{Syntax.ambiguity\_limit}\verb|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.
+ Terms that cannot be type-checked are filtered out, which often
+ leads to a unique result in the end. Unlike regular type
+ reconstruction, which is applied to the whole collection of input
+ terms simultaneously, the filtering stage only treats each given
+ term in isolation. Filtering is also not attempted for individual
+ types or raw ASTs (as required for \hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}).
+
+ Certain warning or error messages are printed, depending on the
+ situation and the given configuration options. Parsing ultimately
+ fails, if multiple results remain after the filtering phase.
+
+ \begin{description}
+
+ \item \hyperlink{attribute.syntax-ambiguity-level}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}ambiguity{\isaliteral{5F}{\isacharunderscore}}level}}} determines the number of
+ parser results that are tolerated without printing a detailed
+ message.
+
+ \item \verb|Syntax.ambiguity_limit| determines the number of
+ resulting parse trees that are shown as part of the printed message
+ in case of an ambiguity.
+
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\isamarkupsection{Raw syntax and translations \label{sec:syn-trans}%
}
\isamarkuptrue%
--- a/doc-src/Ref/defining.tex Sat Feb 04 18:33:04 2012 +0100
+++ b/doc-src/Ref/defining.tex Sun Feb 05 18:11:19 2012 +0100
@@ -83,54 +83,6 @@
{\out exp = "-" exp[3] => "-" (3)}
\end{ttbox}
-
-\section{Ambiguity of parsed expressions} \label{sec:ambiguity}
-\index{ambiguity!of parsed expressions}
-
-To keep the grammar small and allow common productions to be shared
-all logical types (except {\tt prop}) are internally represented
-by one nonterminal, namely {\tt logic}. This and omitted or too freely
-chosen priorities may lead to ways of parsing an expression that were
-not intended by the theory's maker. In most cases Isabelle is able to
-select one of multiple parse trees that an expression has lead
-to by checking which of them can be typed correctly. But this may not
-work in every case and always slows down parsing.
-The warning and error messages that can be produced during this process are
-as follows:
-
-If an ambiguity can be resolved by type inference the following
-warning is shown to remind the user that parsing is (unnecessarily)
-slowed down. In cases where it's not easily possible to eliminate the
-ambiguity the frequency of the warning can be controlled by changing
-the value of {\tt Syntax.ambiguity_level} which has type {\tt int
-ref}. Its default value is 1 and by increasing it one can control how
-many parse trees are necessary to generate the warning.
-
-\begin{ttbox}
-{\out Ambiguous input "\dots"}
-{\out produces the following parse trees:}
-{\out \dots}
-{\out Fortunately, only one parse tree is type correct.}
-{\out You may still want to disambiguate your grammar or your input.}
-\end{ttbox}
-
-The following message is normally caused by using the same
-syntax in two different productions:
-
-\begin{ttbox}
-{\out Ambiguous input "..."}
-{\out produces the following parse trees:}
-{\out \dots}
-{\out More than one term is type correct:}
-{\out \dots}
-\end{ttbox}
-
-Ambiguities occuring in syntax translation rules cannot be resolved by
-type inference because it is not necessary for these rules to be type
-correct. Therefore Isabelle always generates an error message and the
-ambiguity should be eliminated by changing the grammar or the rule.
-
-
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "ref"