src/Pure/Syntax/syntax.ML
changeset 46512 4f9f61f9b535
parent 46506 c7faa011bfa7
child 46849 36f392239b6a
     1.1 --- a/src/Pure/Syntax/syntax.ML	Fri Feb 17 11:24:39 2012 +0100
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Fri Feb 17 15:42:26 2012 +0100
     1.3 @@ -10,8 +10,8 @@
     1.4    type operations
     1.5    val install_operations: operations -> unit
     1.6    val root: string Config.T
     1.7 -  val ambiguity_raw: Config.raw
     1.8 -  val ambiguity: string Config.T
     1.9 +  val ambiguity_warning_raw: Config.raw
    1.10 +  val ambiguity_warning: bool Config.T
    1.11    val ambiguity_limit_raw: Config.raw
    1.12    val ambiguity_limit: int Config.T
    1.13    val read_token: string -> Symbol_Pos.T list * Position.T
    1.14 @@ -155,8 +155,8 @@
    1.15  
    1.16  val root = Config.string (Config.declare "syntax_root" (K (Config.String "any")));
    1.17  
    1.18 -val ambiguity_raw = Config.declare "syntax_ambiguity" (fn _ => Config.String "warning");
    1.19 -val ambiguity = Config.string ambiguity_raw;
    1.20 +val ambiguity_warning_raw = Config.declare "syntax_ambiguity_warning" (fn _ => Config.Bool true);
    1.21 +val ambiguity_warning = Config.bool ambiguity_warning_raw;
    1.22  
    1.23  val ambiguity_limit_raw = Config.declare "syntax_ambiguity_limit" (fn _ => Config.Int 10);
    1.24  val ambiguity_limit = Config.int ambiguity_limit_raw;