src/Pure/Syntax/syntax.ML

--- a/src/Pure/Syntax/syntax.ML	Thu Feb 16 17:09:15 2012 +0100
+++ b/src/Pure/Syntax/syntax.ML	Thu Feb 16 22:18:28 2012 +0100
@@ -10,12 +10,10 @@
   type operations
   val install_operations: operations -> unit
   val root: string Config.T
-  val ambiguity_enabled: bool Config.T
-  val ambiguity_level_raw: Config.raw
-  val ambiguity_level: int Config.T
+  val ambiguity_raw: Config.raw
+  val ambiguity: string Config.T
+  val ambiguity_limit_raw: Config.raw
   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
@@ -157,19 +155,11 @@
 
 val root = Config.string (Config.declare "syntax_root" (K (Config.String "any")));
 
-val ambiguity_enabled =
-  Config.bool (Config.declare "syntax_ambiguity_enabled" (fn _ => Config.Bool true));
-
-val ambiguity_level_raw = Config.declare "syntax_ambiguity_level" (fn _ => Config.Int 1);
-val ambiguity_level = Config.int ambiguity_level_raw;
+val ambiguity_raw = Config.declare "syntax_ambiguity" (fn _ => Config.String "warning");
+val ambiguity = Config.string ambiguity_raw;
 
-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;
+val ambiguity_limit_raw = Config.declare "syntax_ambiguity_limit" (fn _ => Config.Int 10);
+val ambiguity_limit = Config.int ambiguity_limit_raw;
 
 
 (* outer syntax token -- with optional YXML content *)