# HG changeset patch
# User kleing
# Date 1312638488 -7200
# Node ID d7c7ec248ef044fd037af64808a1fcdcc44c1c1e
# Parent  dc0a73004c94716010c8535e4fc0a2ea842843f3
make syntax ambiguity warnings a config option

diff -r dc0a73004c94 -r d7c7ec248ef0 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Mon Aug 08 11:47:41 2011 -0700
+++ b/src/Pure/Isar/attrib.ML	Sat Aug 06 15:48:08 2011 +0200
@@ -444,6 +444,7 @@
   register_config Printer.show_structs_raw #>
   register_config Printer.show_question_marks_raw #>
   register_config Syntax.ambiguity_level_raw #>
+  register_config Syntax.ambiguity_warnings_raw #>
   register_config Syntax_Trans.eta_contract_raw #>
   register_config Name_Space.names_long_raw #>
   register_config Name_Space.names_short_raw #>
diff -r dc0a73004c94 -r d7c7ec248ef0 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Mon Aug 08 11:47:41 2011 -0700
+++ b/src/Pure/Syntax/syntax.ML	Sat Aug 06 15:48:08 2011 +0200
@@ -16,6 +16,8 @@
   val ambiguity_level_raw: Config.raw
   val ambiguity_level: int Config.T
   val ambiguity_limit: int Config.T
+  val ambiguity_warnings_raw: Config.raw
+  val ambiguity_warnings: bool Config.T
   val read_token: string -> Symbol_Pos.T list * Position.T
   val parse_token: Proof.context -> (XML.tree list -> 'a) ->
     Markup.T -> (Symbol_Pos.T list * Position.T -> 'a) -> string -> 'a
@@ -193,6 +195,11 @@
 val ambiguity_limit =
   Config.int (Config.declare "syntax_ambiguity_limit" (fn _ => Config.Int 10));
 
+val ambiguity_warnings_raw = 
+  Config.declare "syntax_ambiguity_warnings" (fn _ => Config.Bool true);
+val ambiguity_warnings =
+  Config.bool ambiguity_warnings_raw;
+
 
 (* outer syntax token -- with optional YXML content *)
 
diff -r dc0a73004c94 -r d7c7ec248ef0 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Mon Aug 08 11:47:41 2011 -0700
+++ b/src/Pure/Syntax/syntax_phases.ML	Sat Aug 06 15:48:08 2011 +0200
@@ -288,15 +288,17 @@
     val len = length pts;
 
     val limit = Config.get ctxt Syntax.ambiguity_limit;
+    val warnings = Config.get ctxt Syntax.ambiguity_warnings;
     val _ =
       if len <= Config.get ctxt Syntax.ambiguity_level then ()
       else if not (Config.get ctxt Syntax.ambiguity_enabled) then error (ambiguity_msg pos)
-      else
+      else if warnings then
         (Context_Position.if_visible ctxt warning (cat_lines
           (("Ambiguous input" ^ Position.str_of pos ^
             "\nproduces " ^ string_of_int len ^ " parse trees" ^
             (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
-            map (Pretty.string_of o Parser.pretty_parsetree) (take limit pts))));
+            map (Pretty.string_of o Parser.pretty_parsetree) (take limit pts))))
+      else ();
 
     val constrain_pos = not raw andalso Config.get ctxt Syntax.positions;
     val parsetree_to_ast = parsetree_to_ast ctxt constrain_pos ast_tr;
@@ -353,6 +355,7 @@
 
           val level = Config.get ctxt Syntax.ambiguity_level;
           val limit = Config.get ctxt Syntax.ambiguity_limit;
+          val warnings = Config.get ctxt Syntax.ambiguity_warnings;
 
           val ambig_msg =
             if ambiguity > 1 andalso ambiguity <= level then
@@ -381,7 +384,7 @@
             report_result ctxt pos
               [(reports', Exn.Exn (Exn.EXCEPTIONS (map ERROR ambig_msg @ errs)))]
           else if len = 1 then
-            (if ambiguity > level then
+            (if ambiguity > level andalso warnings then
               Context_Position.if_visible ctxt warning
                 "Fortunately, only one parse tree is type correct.\n\
                 \You may still want to disambiguate your grammar or your input."