doc-src/IsarRef/Thy/Inner_Syntax.thy

 
 subsection {* Ambiguity of parsed expressions *}
 
 text {*
   \begin{tabular}{rcll}
-    @{attribute_def syntax_ambiguity} & : & @{text attribute} & default @{text warning} \\
+    @{attribute_def syntax_ambiguity_warning} & : & @{text attribute} & default @{text true} \\
     @{attribute_def syntax_ambiguity_limit} & : & @{text attribute} & default @{text 10} \\
   \end{tabular}
 
   Depending on the grammar and the given input, parsing may be
   ambiguous.  Isabelle lets the Earley parser enumerate all possible

   situation and the given configuration options.  Parsing ultimately
   fails, if multiple results remain after the filtering phase.
 
   \begin{description}
 
-  \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 @{attribute syntax_ambiguity_warning} controls output of
+  explicit warning messages about syntax ambiguity.
 
   \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.