added reference variable ambiguity_level to control ambiguity warnings
authorclasohm
Thu Jan 26 12:44:50 1995 +0100 (1995-01-26)
changeset 87927675591cc50
parent 878 7c82ab7602b4
child 880 667dc43e3b98
added reference variable ambiguity_level to control ambiguity warnings
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Wed Jan 25 04:00:27 1995 +0100
     1.2 +++ b/src/Pure/sign.ML	Thu Jan 26 12:44:50 1995 +0100
     1.3 @@ -64,6 +64,7 @@
     1.4      val pure: sg
     1.5      val const_of_class: class -> string
     1.6      val class_of_const: string -> class
     1.7 +    val ambiguity_level: int ref
     1.8    end
     1.9  end;
    1.10  
    1.11 @@ -244,6 +245,8 @@
    1.12  
    1.13  (** infer_types **)         (*exception ERROR*)
    1.14  
    1.15 +val ambiguity_level = ref 1;
    1.16 +
    1.17  fun infer_types sg types sorts print_msg (ts, T) =
    1.18    let
    1.19      val Sg {tsig, ...} = sg;
    1.20 @@ -294,7 +297,7 @@
    1.21            else error msg;
    1.22  
    1.23      val (idx, infrd_t, tye) = process_terms ts (None, None, None) "" 0;
    1.24 -  in if print_msg andalso length ts > 1 then
    1.25 +  in if print_msg andalso length ts > !ambiguity_level then
    1.26         writeln "Fortunately, only one parse tree is type correct.\n\
    1.27           \It helps (speed!) if you disambiguate your grammar or your input."
    1.28       else ();