doc-src/IsarRef/Thy/document/Inner_Syntax.tex
changeset 46512 4f9f61f9b535
parent 46506 c7faa011bfa7
child 46525 af3df09590f9
     1.1 --- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Fri Feb 17 11:24:39 2012 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Fri Feb 17 15:42:26 2012 +0100
     1.3 @@ -1154,7 +1154,7 @@
     1.4  %
     1.5  \begin{isamarkuptext}%
     1.6  \begin{tabular}{rcll}
     1.7 -    \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.8 +    \indexdef{}{attribute}{syntax\_ambiguity\_warning}\hypertarget{attribute.syntax-ambiguity-warning}{\hyperlink{attribute.syntax-ambiguity-warning}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}ambiguity{\isaliteral{5F}{\isacharunderscore}}warning}}}} & : & \isa{attribute} & default \isa{true} \\
     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 @@ -1174,8 +1174,8 @@
    1.13  
    1.14    \begin{description}
    1.15  
    1.16 -  \item \hyperlink{attribute.syntax-ambiguity}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}ambiguity}}} determines reaction on multiple
    1.17 -  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.18 +  \item \hyperlink{attribute.syntax-ambiguity-warning}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}ambiguity{\isaliteral{5F}{\isacharunderscore}}warning}}} controls output of
    1.19 +  explicit warning messages about syntax ambiguity.
    1.20  
    1.21    \item \hyperlink{attribute.syntax-ambiguity-limit}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}ambiguity{\isaliteral{5F}{\isacharunderscore}}limit}}} determines the number of
    1.22    resulting parse trees that are shown as part of the printed message