src/Pure/sign.ML
changeset 952 9e10962866b0
parent 949 83c588d6fee9
child 959 35c2e5e114c4
     1.1 --- a/src/Pure/sign.ML	Tue Mar 14 09:47:28 1995 +0100
     1.2 +++ b/src/Pure/sign.ML	Tue Mar 14 10:40:04 1995 +0100
     1.3 @@ -272,52 +272,47 @@
     1.4  
     1.5      val ct = const_type sg;
     1.6  
     1.7 -    fun process_terms (t::ts) (idx, infrd_t, tye) msg n =
     1.8 -         let val (infrd_t', tye', msg') = 
     1.9 -              let val (T,tye) =
    1.10 -                    Type.infer_types(tsig,ct,types,sorts,used,freeze,T',t)
    1.11 -              in (Some T, Some tye, msg) end
    1.12 -              handle TYPE arg => (None, None, exn_type_msg arg)
    1.13 -
    1.14 -             val old_show_brackets = !show_brackets;
    1.15 +    fun warn() =
    1.16 +      if length ts > 1 andalso length ts <= !Syntax.ambiguity_level
    1.17 +      then (*no warning shown yet*)
    1.18 +           writeln "Warning: Currently parsed input \
    1.19 +                   \produces more than one parse tree.\n\
    1.20 +                   \For more information lower Syntax.ambiguity_level."
    1.21 +      else ();
    1.22  
    1.23 -             val _ = (show_brackets := true);
    1.24 -
    1.25 -             val msg'' = 
    1.26 -               if is_none idx then (if is_none infrd_t' then msg' else "")
    1.27 -               else if is_none infrd_t' then "" 
    1.28 -               else (if msg' = "" then 
    1.29 -                "Error: More than one term is type correct:\n" ^
    1.30 -                (show_term (the infrd_t)) else msg') ^ "\n" ^ 
    1.31 -                (show_term (the infrd_t')) ^ "\n";
    1.32 +    datatype result = One of int * term * (indexname * typ) list
    1.33 +                    | Errs of (string * typ list * term list)list
    1.34 +                    | Ambigs of term list;
    1.35  
    1.36 -         in show_brackets := old_show_brackets;
    1.37 -            if is_none infrd_t' then
    1.38 -              process_terms ts (idx, infrd_t, tye) msg'' (n+1)
    1.39 -            else
    1.40 -              process_terms ts (Some n, infrd_t', tye') msg'' (n+1)
    1.41 -         end
    1.42 -      | process_terms [] (idx, infrd_t, tye) msg _ = 
    1.43 -          if msg = "" then (the idx, the infrd_t, the tye) 
    1.44 -          else
    1.45 -            (if length ts > 1 andalso length ts <= !Syntax.ambiguity_level then
    1.46 -                                                      (*no warning shown yet?*)
    1.47 -               writeln "Warning: Currently parsed input \
    1.48 -                       \produces more than one parse tree.\n\
    1.49 -                       \For more information lower Syntax.ambiguity_level."
    1.50 -             else ();
    1.51 -             error msg)
    1.52 +    fun process_term(res,(t,i)) =
    1.53 +       let val (u,tye) = Type.infer_types(tsig,ct,types,sorts,used,freeze,T',t)
    1.54 +       in case res of
    1.55 +            One(_,t0,_) => Ambigs([u,t0])
    1.56 +          | Errs _ => One(i,u,tye)
    1.57 +          | Ambigs(us) => Ambigs(u::us)
    1.58 +       end
    1.59 +       handle TYPE arg => (case res of Errs(errs) => Errs(arg::errs)
    1.60 +                                     | _ => res);
    1.61  
    1.62 -    val (idx, infrd_t, tye) = process_terms ts (None, None, None) "" 0;
    1.63 -  in if print_msg andalso length ts > !Syntax.ambiguity_level then
    1.64 -       writeln "Fortunately, only one parse tree is type correct.\n\
    1.65 -         \It helps (speed!) if you disambiguate your grammar or your input."
    1.66 -     else ();
    1.67 -     (idx, infrd_t, tye)
    1.68 +  in case foldl process_term (Errs[], ts ~~ (0 upto (length ts - 1))) of
    1.69 +       One(res) =>
    1.70 +         (if length ts > !Syntax.ambiguity_level
    1.71 +          then writeln "Fortunately, only one parse tree is type correct.\n\
    1.72 +            \It helps (speed!) if you disambiguate your grammar or your input."
    1.73 +          else ();
    1.74 +          res)
    1.75 +     | Errs(errs) => (warn(); error(cat_lines(map exn_type_msg errs)))
    1.76 +     | Ambigs(us) =>
    1.77 +         (warn();
    1.78 +          let val old_show_brackets = !show_brackets
    1.79 +              val _ = show_brackets := true;
    1.80 +              val errs = cat_lines(map show_term us)
    1.81 +          in show_brackets := old_show_brackets;
    1.82 +             error("Error: More than one term is type correct:\n" ^ errs)
    1.83 +          end)
    1.84    end;
    1.85  
    1.86  
    1.87 -
    1.88  (** extend signature **)    (*exception ERROR*)
    1.89  
    1.90  (** signature extension functions **)  (*exception ERROR*)