1.1 --- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Thu Feb 16 17:09:15 2012 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Thu Feb 16 22:18:28 2012 +0100
     1.3 @@ -1154,13 +1154,10 @@
     1.4  %
     1.5  \begin{isamarkuptext}%
     1.6  \begin{tabular}{rcll}
     1.7 -    \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}}} \\
     1.8 +    \indexdef{}{attribute}{syntax\_ambiguity}\hypertarget{attribute.syntax-ambiguity}{\hyperlink{attribute.syntax-ambiguity}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}ambiguity}}}} & : & \isa{attribute} & default \isa{warning} \\
     1.9 +    \indexdef{}{attribute}{syntax\_ambiguity\_limit}\hypertarget{attribute.syntax-ambiguity-limit}{\hyperlink{attribute.syntax-ambiguity-limit}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}ambiguity{\isaliteral{5F}{\isacharunderscore}}limit}}}} & : & \isa{attribute} & default \isa{{\isadigit{1}}{\isadigit{0}}} \\
    1.10    \end{tabular}
    1.11  
    1.12 -  \begin{mldecls}
    1.13 -    \indexdef{}{ML}{Syntax.ambiguity\_limit}\verb|Syntax.ambiguity_limit: int Config.T| \\  %FIXME attribute
    1.14 -  \end{mldecls}
    1.15 -
    1.16    Depending on the grammar and the given input, parsing may be
    1.17    ambiguous.  Isabelle lets the Earley parser enumerate all possible
    1.18    parse trees, and then tries to make the best out of the situation.
    1.19 @@ -1177,11 +1174,10 @@
    1.20  
    1.21    \begin{description}
    1.22  
    1.23 -  \item \hyperlink{attribute.syntax-ambiguity-level}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}ambiguity{\isaliteral{5F}{\isacharunderscore}}level}}} determines the number of
    1.24 -  parser results that are tolerated without printing a detailed
    1.25 -  message.
    1.26 +  \item \hyperlink{attribute.syntax-ambiguity}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}ambiguity}}} determines reaction on multiple
    1.27 +  results of parsing; this string option can be set to \isa{{\isaliteral{22}{\isachardoublequote}}ignore{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}warning{\isaliteral{22}{\isachardoublequote}}}, or \isa{{\isaliteral{22}{\isachardoublequote}}error{\isaliteral{22}{\isachardoublequote}}}.
    1.28  
    1.29 -  \item \verb|Syntax.ambiguity_limit| determines the number of
    1.30 +  \item \hyperlink{attribute.syntax-ambiguity-limit}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}ambiguity{\isaliteral{5F}{\isacharunderscore}}limit}}} determines the number of
    1.31    resulting parse trees that are shown as part of the printed message
    1.32    in case of an ambiguity.
    1.33