src/Pure/sign.ML
changeset 3552 f348e8a2db4b
parent 2979 db6941221197
child 3791 c5db2c87a646
equal deleted inserted replaced
3551:7c013a617813 3552:f348e8a2db4b
   239     handle ERROR => err_in_type str;
   239     handle ERROR => err_in_type str;
   240 
   240 
   241 (*read and certify typ wrt a signature*)
   241 (*read and certify typ wrt a signature*)
   242 fun read_typ (Sg {tsig, syn, ...}, sort_of) str =
   242 fun read_typ (Sg {tsig, syn, ...}, sort_of) str =
   243   Type.cert_typ tsig (read_raw_typ syn tsig sort_of str)
   243   Type.cert_typ tsig (read_raw_typ syn tsig sort_of str)
   244     handle TYPE (msg, _, _) => (writeln msg; err_in_type str);
   244     handle TYPE (msg, _, _) => (error_msg msg; err_in_type str);
   245 
   245 
   246 
   246 
   247 
   247 
   248 (** certify types and terms **)   (*exception TYPE*)
   248 (** certify types and terms **)   (*exception TYPE*)
   249 
   249 
   369         | _ => res);
   369         | _ => res);
   370   in
   370   in
   371     (case foldl process_term (Errs [], ts ~~ (0 upto (length ts - 1))) of
   371     (case foldl process_term (Errs [], ts ~~ (0 upto (length ts - 1))) of
   372       One res =>
   372       One res =>
   373        (if length ts > ! Syntax.ambiguity_level then
   373        (if length ts > ! Syntax.ambiguity_level then
   374           writeln "Fortunately, only one parse tree is type correct.\n\
   374           warning "Fortunately, only one parse tree is type correct.\n\
   375             \It helps (speed!) if you disambiguate your grammar or your input."
   375             \It helps (speed!) if you disambiguate your grammar or your input."
   376         else (); res)
   376         else (); res)
   377     | Errs errs => (warn (); error (cat_lines errs))
   377     | Errs errs => (warn (); error (cat_lines errs))
   378     | Ambigs us =>
   378     | Ambigs us =>
   379         (warn (); error ("Error: More than one term is type correct:\n" ^
   379         (warn (); error ("Error: More than one term is type correct:\n" ^
   452 fun ext_cnsts rd_const syn_only prmode (syn, tsig, ctab) raw_consts =
   452 fun ext_cnsts rd_const syn_only prmode (syn, tsig, ctab) raw_consts =
   453   let
   453   let
   454     fun prep_const (c, ty, mx) =
   454     fun prep_const (c, ty, mx) =
   455      (c, compress_type (Type.varifyT (Type.cert_typ tsig (Type.no_tvars ty))), mx)
   455      (c, compress_type (Type.varifyT (Type.cert_typ tsig (Type.no_tvars ty))), mx)
   456        handle TYPE (msg, _, _)
   456        handle TYPE (msg, _, _)
   457          => (writeln msg; err_in_const (Syntax.const_name c mx));
   457          => (error_msg msg; err_in_const (Syntax.const_name c mx));
   458 
   458 
   459     val consts = map (prep_const o rd_const syn tsig) raw_consts;
   459     val consts = map (prep_const o rd_const syn tsig) raw_consts;
   460     val decls =
   460     val decls =
   461       if syn_only then []
   461       if syn_only then []
   462       else filter_out (equal "" o fst) (decls_of Syntax.const_name consts);
   462       else filter_out (equal "" o fst) (decls_of Syntax.const_name consts);