src/Pure/sign.ML
changeset 18678 dd0c569fa43d
parent 18667 85d04c28224a
child 18714 1c310b042d69
     1.1 --- a/src/Pure/sign.ML	Fri Jan 13 17:39:41 2006 +0100
     1.2 +++ b/src/Pure/sign.ML	Sat Jan 14 17:14:06 2006 +0100
     1.3 @@ -477,7 +477,7 @@
     1.4      val get_sort = TypeInfer.get_sort (tsig_of thy) def_sort (intern_sort thy);
     1.5      val T = intern_tycons thy (Syntax.read_typ thy syn get_sort (intern_sort thy) str);
     1.6    in cert thy T handle TYPE (msg, _, _) => error msg end
     1.7 -  handle ERROR => error ("The error(s) above occurred in type " ^ quote str);
     1.8 +  handle ERROR msg => cat_error msg ("The error(s) above occurred in type " ^ quote str);
     1.9  
    1.10  fun gen_read_typ cert (thy, def_sort) str =
    1.11    gen_read_typ' cert (syn_of thy) (thy, def_sort) str;
    1.12 @@ -531,31 +531,29 @@
    1.13      val typs =
    1.14        map (fn (_, T) => certify_typ thy T handle TYPE (msg, _, _) => error msg) args;
    1.15  
    1.16 -    fun infer ts = OK (TypeInfer.infer_types (Syntax.pp_show_brackets pp) (tsig_of thy)
    1.17 +    fun infer ts = Result (TypeInfer.infer_types (Syntax.pp_show_brackets pp) (tsig_of thy)
    1.18          (const_constraint thy) def_type def_sort (intern_const thy) (intern_tycons thy)
    1.19          (intern_sort thy) used freeze typs ts)
    1.20 -      handle TYPE (msg, _, _) => Error msg;
    1.21 +      handle TYPE (msg, _, _) => Exn (ERROR msg);
    1.22  
    1.23      val err_results = map infer termss;
    1.24 -    val errs = List.mapPartial get_error err_results;
    1.25 -    val results = List.mapPartial get_ok err_results;
    1.26 +    val errs = List.mapPartial (fn Exn (ERROR msg) => SOME msg | _ => NONE) err_results;
    1.27 +    val results = List.mapPartial get_result err_results;
    1.28  
    1.29      val ambiguity = length termss;
    1.30 -
    1.31      fun ambig_msg () =
    1.32 -      if ambiguity > 1 andalso ambiguity <= ! Syntax.ambiguity_level
    1.33 -      then
    1.34 -        error_msg "Got more than one parse tree.\n\
    1.35 -          \Retry with smaller Syntax.ambiguity_level for more information."
    1.36 -      else ();
    1.37 +      if ambiguity > 1 andalso ambiguity <= ! Syntax.ambiguity_level then
    1.38 +        "Got more than one parse tree.\n\
    1.39 +        \Retry with smaller Syntax.ambiguity_level for more information."
    1.40 +      else "";
    1.41    in
    1.42 -    if null results then (ambig_msg (); error (cat_lines errs))
    1.43 +    if null results then (cat_error (ambig_msg ()) (cat_lines errs))
    1.44      else if length results = 1 then
    1.45        (if ambiguity > ! Syntax.ambiguity_level then
    1.46          warning "Fortunately, only one parse tree is type correct.\n\
    1.47            \You may still want to disambiguate your grammar or your input."
    1.48        else (); hd results)
    1.49 -    else (ambig_msg (); error ("More than one term is type correct:\n" ^
    1.50 +    else (cat_error (ambig_msg ()) ("More than one term is type correct:\n" ^
    1.51        cat_lines (map (Pretty.string_of_term pp) (List.concat (map fst results)))))
    1.52    end;
    1.53  
    1.54 @@ -578,7 +576,7 @@
    1.55  fun simple_read_term thy T s =
    1.56    let val ([t], _) = read_def_terms (thy, K NONE, K NONE) [] true [(s, T)]
    1.57    in t end
    1.58 -  handle ERROR => error ("The error(s) above occurred for term " ^ s);
    1.59 +  handle ERROR msg => cat_error msg ("The error(s) above occurred for term " ^ s);
    1.60  
    1.61  fun read_term thy = simple_read_term thy TypeInfer.logicT;
    1.62  fun read_prop thy = simple_read_term thy propT;
    1.63 @@ -630,7 +628,7 @@
    1.64        val syn' = Syntax.extend_type_gram [(a, length vs, mx)] syn;
    1.65        val a' = Syntax.type_name a mx;
    1.66        val abbr = (a', vs, prep_typ thy rhs)
    1.67 -        handle ERROR => error ("in type abbreviation " ^ quote a');
    1.68 +        handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote a');
    1.69        val tsig' = Type.add_abbrevs naming [abbr] tsig;
    1.70      in (naming, syn', tsig', consts) end);
    1.71  
    1.72 @@ -643,7 +641,7 @@
    1.73  fun gen_add_arities int_type prep_sort arities thy = thy |> map_tsig (fn tsig =>
    1.74    let
    1.75      fun prep_arity (a, Ss, S) = (int_type thy a, map (prep_sort thy) Ss, prep_sort thy S)
    1.76 -      handle ERROR => error ("in arity for type " ^ quote a);
    1.77 +      handle ERROR msg => cat_error msg ("in arity for type " ^ quote a);
    1.78      val tsig' = Type.add_arities (pp thy) (map prep_arity arities) tsig;
    1.79    in tsig' end);
    1.80  
    1.81 @@ -655,8 +653,8 @@
    1.82  
    1.83  fun gen_syntax change_gram prep_typ prmode args thy =
    1.84    let
    1.85 -    fun prep (c, T, mx) = (c, prep_typ thy T, mx)
    1.86 -      handle ERROR => error ("in syntax declaration " ^ quote (Syntax.const_name c mx));
    1.87 +    fun prep (c, T, mx) = (c, prep_typ thy T, mx) handle ERROR msg =>
    1.88 +      cat_error msg ("in syntax declaration " ^ quote (Syntax.const_name c mx));
    1.89    in thy |> map_syn (change_gram (is_logtype thy) prmode (map prep args)) end;
    1.90  
    1.91  fun gen_add_syntax x = gen_syntax Syntax.extend_const_gram x;
    1.92 @@ -677,7 +675,8 @@
    1.93    let
    1.94      val prepT = Compress.typ thy o Type.varifyT o Type.no_tvars o Term.no_dummyT o prep_typ thy;
    1.95      fun prep (c, T, mx) = ((c, prepT T, mx) handle TYPE (msg, _, _) => error msg)
    1.96 -      handle ERROR => error ("in declaration of constant " ^ quote (Syntax.const_name c mx));
    1.97 +      handle ERROR msg =>
    1.98 +        cat_error msg ("in declaration of constant " ^ quote (Syntax.const_name c mx));
    1.99      val args = map prep raw_args;
   1.100      val decls = args |> map (fn (c, T, mx) => (Syntax.const_name c mx, T));
   1.101    in