moved ambiguity_level to Syntax/syntax.ML
authorclasohm
Fri Jan 27 12:28:05 1995 +0100 (1995-01-27)
changeset 881d7dcba167ed8
parent 880 667dc43e3b98
child 882 b118d1ea0dfd
moved ambiguity_level to Syntax/syntax.ML
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Thu Jan 26 13:31:36 1995 +0100
     1.2 +++ b/src/Pure/sign.ML	Fri Jan 27 12:28:05 1995 +0100
     1.3 @@ -64,7 +64,6 @@
     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 @@ -245,8 +244,6 @@
    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,10 +291,17 @@
    1.21           end
    1.22        | process_terms [] (idx, infrd_t, tye) msg _ = 
    1.23            if msg = "" then (the idx, the infrd_t, the tye) 
    1.24 -          else error msg;
    1.25 +          else
    1.26 +            (if length ts <= !Syntax.ambiguity_level then
    1.27 +                                                      (*no warning shown yet?*)
    1.28 +               writeln "Warning: Currently parsed input \
    1.29 +                       \produces more than one parse tree.\n\
    1.30 +                       \For more information lower Syntax.ambiguity_level."
    1.31 +             else ();
    1.32 +             error msg)
    1.33  
    1.34      val (idx, infrd_t, tye) = process_terms ts (None, None, None) "" 0;
    1.35 -  in if print_msg andalso length ts > !ambiguity_level then
    1.36 +  in if print_msg andalso length ts > !Syntax.ambiguity_level then
    1.37         writeln "Fortunately, only one parse tree is type correct.\n\
    1.38           \It helps (speed!) if you disambiguate your grammar or your input."
    1.39       else ();