# HG changeset patch
# User wenzelm
# Date 1328461879 -3600
# Node ID a1827b8b45aeeaee03515f14b0c9644216e4422f
# Parent  465851ba524e4829c491c8d56558f4ef437c12fc
updated section about syntax ambiguity;

diff -r 465851ba524e -r a1827b8b45ae doc-src/IsarRef/Thy/Inner_Syntax.thy
--- 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 {*
diff -r 465851ba524e -r a1827b8b45ae doc-src/IsarRef/Thy/document/Inner_Syntax.tex
--- 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%
diff -r 465851ba524e -r a1827b8b45ae doc-src/Ref/defining.tex
--- 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"