--- 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 *)